CSE647: Testing and Verification
		     Homework 3 (ver. 19 Sep, 15:30)         Due 26 Sep
			      Scott Stoller

1. Give an example of a program that contains some variable v and that
has two different executions sigma1 and sigma2 such that the lockset
associated with v at the end of sigma1 is different than the lockset
associated with v at the end of sigma2.  Note: The lockset algorithm
does not halt the program when it detects a violation of the locking
discipline; a warning is generated and the program continues to execute
normally.  Assume the lockset algorithm is as in section 2.2 of the Eraser 
paper.

2. Let bexp be an expression of type "bool".  Let lv be a variable of type
"lock".  Consider the code fragments

lv.acquire();
if (bexp) stmt;                         (1)
lv.release();

and

if (bexp) {
  lv.acquire();
  if (bexp) stmt;                       (2)
  lv.release();
}

Note that (2) is more likely than (1) to have a race.

a. Under what conditions is (2) preferable to (1)?

b. Under what conditions are (1) and (2) equivalent (ignoring performance)?
A reasonable set of sufficient conditions is fine.
You do not need to find a set of necessary and sufficient conditions.