Interference
Interference
The problem in the Ornamental Gardens program is that we have permitted the increment action by the West Turnstile to overlap with the increment action of East.
GARDEN = EAST || WEST
where
EAST = (increment ® EAST)
WEST = (increment ® WEST)
and
increment = (read ® add1 ® write)
Consequently the following is a legal execution trace:
Wread ® Eread ® Wadd1 ® Wwrite ® Eadd1 ® Ewrite
It can easily be seen that this results in losing an increment on value_. For correctness, we require that the increment actions do not overlap.
forall e: (Wincrement ® Eincrement) or (Eincrement ® Wincrement)