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, which let you assert properties on how variables
change in a step.)
H
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