Re: [tlaplus] Patterns for detecting data race with TLA+?

[Shuhao Wu <shuhao@xxxxxxxxxxxx>]

Thanks Hillel for the suggestion. Your blog post is also very 
enlightening, especially on the forbidden state transition checks that I 
also struggled with[1].

For my problem though, the race conditions that occur in real-life seem 
difficult to model with TLA directly. For example, if I read/write to a 
large (multi-word) variable in something like C/C++ without explicit 
synchronization, it can result in a torn-read. Without synchronization, 
the compiler may even re-order and/or optimize the statements in 
unpredictable (undefined) manners. Since in TLA+, the variable values 
are usually abstract values, it seems difficult to me to model the 
actual "bad" event.

I suppose what I could do is to create an auxiliary variable that 
increments and then decrements with each read and write operation, which 
may require splitting the read/write operations into multiple steps for 
the aux variable. Then I can use an invariant to assert that the aux 
variable never increases above 1 to ensure synchronization is properly 
implement. Not 100% sure if this is the simplest approach as I have yet 
to test it, but it might be an acceptable work around for this purpose.

Thanks again,
Shuhao

[1] I've worked on an unfinished post detailing my journey on 
discovering how to write temporaral properties that specifying 
conditions like A leads to B and remains at B, or A leads to B at least 
once. Once I get it done, I may ask for more feedback here.

On 2022-05-27 17:45, Hillel Wayne wrote:
> Hi Shuhao,
>
> Your spec doesn't /necessarily/ mean the two variables are reading and 
> writing the same variable at the same time. Remember, each label 
> represents an /abstract/ amount of time: for all you know the two 
> actions could be two years apart. It's a good proxy for bad behavior, 
> but it's still an "indirect" property.
>
> I find that "direct properties" scale better. What is the bad state that 
> both processes writing at the same time would /cause/? If you check 
> /that/ as an invariant, race conditions will naturally appear in the 
> error trace. You can then write indirect properties for the specific 
> race conditions you see to make them trigger earlier in the model checking.
>
> (One useful tool for this is Action Properties 
> <https://www.hillelwayne.com/post/action-properties/>, which let you 
> assert properties on how variables change in a step.)
>
> H
>
> On 5/27/2022 4:13 PM, Shuhao Wu wrote:
> > Hello all:
> >
> > I'm currently working on some lock-less algorithms with TLA+ 
> > (specifically, with PlusCal). One of the things that needs to be 
> > checked is that the algorithm is data-race-free, where no two 
> > processes (in PlusCal terms) are reading and writing to the same 
> > variable at the same time. Here's a sample spec with a data race on 
> > the Global2 variable:
> >
> > variables Global1 = 0, Global2 = 0;
> >
> > fair process A = "A"
> >   variable local;
> > begin
> >   A1:
> >     local := Global1;
> >   A2:
> >     Global2 := 10;
> > end process;
> >
> > fair process B = "B"
> >   variable local;
> > begin
> >   B1:
> >     local := Global1;
> >   B2:
> >     local := Global2;
> > end process;
> >
> > Checking if a data race occurred in TLC is technically as simple as 
> > checking the invariant ~(pc["A"] = "A2" /\ pc["B"] = "B2"). However, I 
> > suspect this doesn't scale very well to specifications with more 
> > variables and states, as you need to manually enumerate every write 
> > (and read) step for the all "global" variables.
> >
> > Is there a known pattern somewhere to check for this class of 
> > problems? My quick googling doesn't show anything. Am I approaching 
> > this problem from an incorrect angle?
> >
> > Thanks,
> >
> > Shuhao
> --
> You received this message because you are subscribed to the Google 
> Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send 
> an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx 
> <mailto:tlaplus+unsubscribe@xxxxxxxxxxxxxxxx>.
> To view this discussion on the web visit 
> https://groups.google.com/d/msgid/tlaplus/6c3f1b9d-7000-1c53-0087-f6882d8afdc9%40gmail.com 
> <https://groups.google.com/d/msgid/tlaplus/6c3f1b9d-7000-1c53-0087-f6882d8afdc9%40gmail.com?utm_medium=email&utm_source=footer>.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/923db76b-4cb2-1256-9130-0a86641d6c6f%40shuhaowu.com.