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)

Previous slide Next slide Back to the first slide View Graphic Version