[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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

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

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.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/6c3f1b9d-7000-1c53-0087-f6882d8afdc9%40gmail.com.