Phase Synchronization for two machines
This is an exercise in formally deriving little multiprograms with the theory of Owicki and Gries and the predicate calculus as our only tools for reasoning. But before we embark on the selected example, we will first explain the Owicki-Gries theory in a very rudimentary fashion.
Unable to display preview. Download preview PDF.