CSE647: Testing and Verification
		   Homework 3 Soln (ver. 2 Oct, 11: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.

Answer: See end of Topic IV (Data races), Section 4.2 (Initialization and
Read-Sharing) of lecture notes.  

sem=0;
theta1: sem.Up    theta2: sem.down
        v++               l.acquire
                          v--  
                          l.release

If theta1 finishes before theta2 starts, then candLockSet(v)={l} at the
end.  If theta1 executes v++ after theta2 finishes, then
candLockSet(v)=empty at the end.

Here's an example from Dezhuang.  This program satisfies LD.  It is based
on the observation that the lockset is not refined during initialization.

theta1: l1.acquire   theta2: l2.acquire
        v++	             v++       
        l1.release           l2.release

If theta1 finishes before theta2 starts, then candLockSet(v)={l2} at the
end.  If they execute in the other order, then candLockSet(v)={l1} at the
end.


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.


Answer:
a. When bexp is usually false, (2) is more efficient than (1).

b.  Here is a set of sufficient conditions.  
 1. bexp has no side effects.  (Everyone forgot about this, but
    I didn't take off points for it.)
 2. bexp contains at most one access to a shared variable.
Comments: 
 1. The example from Ni2 in the Eraser paper presumably satisfies these
    conditions: presumably p is unshared, because they don't mention
    races on p, only on p->ip_fp.
 2. Many other answers are possible.  However, conditions that cannot be
    easily checked by static analysis are less useful.