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
> --
> 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+u...@googlegroups.com
> <mailto:
tlaplus+u...@googlegroups.com>.
> 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>.