> What is the bad
state that both processes writing at the same time would cause?
Normally this is a great idea, but as Shuhao points out, in C/C++ the data race itself is the bad state, since data races are undefined behavior. Even if the data race is benign (in the sense that it does not lead to any bad states in the TLA+ model) you would still want to know about it, since it could cause bad behavior in a real C/C++ implementation.
> splitting the read/write operations into multiple steps
Yes, that is exactly how you would check such a thing in TLA+. PlusCal does not provide a way to express the statement "process P is about to do a read/write to variable X". However, by splitting reads and writes into multiple steps, we can make it possible to write such a statement.
Here's a spec I wrote that uses that idea. It uses auxiliary variables "op" and "addr" to record what each process is about to do before it does it. The extra steps for each read/write do unfortunately increase the state space, but this feels like the right approach to me.
---- MODULE DataRace ----
EXTENDS Naturals, Sequences
(*
--algorithm my_processes
variables
mem = <<0, 0>>,
addr = [p \in ProcSet |-> 0],
op = [p \in ProcSet |-> "none"],
local = [p \in ProcSet |-> 0]; \* return value from read(a)
define
Addr1 == 1
Addr2 == 2
end define
procedure read(a)
begin
start_read:
addr[self] := a;
op[self] := "read";
do_read:
local[self] := mem[a];
op[self] := "none";
addr[self] := 0; \* optional; reduces the state space
return;
end procedure
procedure write(a, value)
begin
start_write:
addr[self] := a;
op[self] := "write";
do_write:
mem[a] := value;
op[self] := "none";
addr[self] := 0; \* optional; reduces the state space
return;
end procedure
fair process A = "A"
begin
A1:
call read(Addr1);
A2:
call write(Addr2, 10);
end process
fair process B = "B"
begin
B1:
call read(Addr1);
B2:
call write(Addr1, 4);
end process
end algorithm
*)
\* BEGIN TRANSLATION
\* END TRANSLATION
\* A data race happens when
\* (1) there are two concurrent operations to the same address and
\* (2) at least one of those operations is a write.
DataRace ==
\E x, y \in ProcSet:
/\ x /= y
/\ op[x] /= "none"
/\ op[y] /= "none"
/\ addr[x] = addr[y]
/\ op[x] = "write" \/ op[y] = "write"
NoDataRace == ~DataRace
====