Lecture Notes for Concurrent Programming

10 June 2003 - Atomicity and Synchronization


If you know that A and B are true, then you know, by the and truth table, that both A and B are true too. and elimination exploits this property by allowing you to conclude either A is true or B is true if you know that A and B is true.

For a co statement, you know that the precondition

{ P1 and P2 and ... and Pn }

is true at the time statement Si begins execution. You can use and elimination to get rid of all the predicates Sj, j != i (as a tactical matter, however, you may want to keep a few of the other predicates in Si's precondition, particularly if you anticipate the need to weaken Si's precondition to avoid interference).


This page last modified on 11 June 2003.