Let's consider a simpler version first: say we have two processes one of which increments x and the other y. X == x' = x+1 Y == y' = y+1 An interleaving specification of the two processes will naturally be written as NextXY_IL == \/ X /\ y' = y \/ Y /\ x' = x A non-interleaving specification that allows both processes to execute simultaneously can be written as NextXY_NI == \/ X /\ [Y]_y \/ Y /\ [X]_x Now let's consider the case where the two processes update a shared variable, similar to your original example XZ == x' = x+1 /\ z' = z+1 YZ == y' = y+1 /\ z' = z-1 The interleaving specification will be similar to the one above: NextXYZ_IL == \/ XZ /\ y' = y \/ YZ /\ x' = x What should the non-interleaving specification be? I don't think there is a unique answer because it is not clear how to reconcile the conflicting updates to the shared variable z. One possible choice would be NextXYZ_NI == \/ (XZ /\ y' = y) \cdot [YZ /\ x' = x]_<<x,y,z>> \/ (YZ /\ x' = x) \cdot [XZ /\ y' = y]_<<x,y,z>> where \cdot is the action composition operator. In other words, the two actions may be performed in a single atomic step, in either order. Expanding the definitions of the actions and of \cdot (which isn't handled by TLC) in the first disjunct, we obtain \E x'',y'',z'' : /\ x'' = x+1 /\ z'' = z+1 /\ y'' = y /\ \/ y' = y''+1 /\ z' = z''-1 /\ x' = x'' \/ x' = x'' /\ y' = y'' /\ z' = z'' which can be simplified to /\ x' = x+1 /\ \/ y' = y /\ z' = z+1 \/ y' = y+1 /\ z' = z \* actually, z' = (z+1)-1 The result for the second disjunct is similar. Note that the formula NextXY_NI above is equivalent to \/ (X /\ y' = y) \cdot [Y /\ x'=x]_<<x,y>> \/ (Y /\ x' = x) \cdot [X /\ y'=y]_<<x,y>> so it appears that the above definition is systematic. But again, I think it is only one possible choice of what one means by non-interleaving composition. If I correctly understand your definition, you let one of the processes update the shared variable and ignore the update coming from the other process. Stephan
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/F6A59C85-D9A7-459B-9861-84C1CA69FD8A%40gmail.com. |