refinementExample.tex

\begin{figure}
\begin{small}
\begin{verbatim}
var Mem[int]:bool; // true: free, false: taken

procedure Test({:cnst "tid"} tid:int) 
{
  call addr1 := Alloc();
  yield;
  call addr2 := Alloc();
  assert addr1 != addr2 && !Mem[addr1] && !Mem[addr2];
}
\end{verbatim}
\end{small}
\caption{Client of \exC{Alloc} and \exC{Free}.}
\label{fig:refTop}
\end{figure}

\begin{figure}
\begin{small}
\begin{verbatim}
var freeSpace:int;
var AtOrAfter[int][int]:bool; 
const tid_max:int, lo:int, hi:int;
axiom lo <= hi;

procedure Alloc({:cnst "tid"} tid:int) returns addr:int
  refines {:atomic} [assume Mem[addr];  
                     Mem[addr] := false;]
{
  Reserve(tid);
  yield AllocInv(tid, addr, freeSpace, AtOrAfter);         
  ptr := lo;
  while (ptr < hi && !found)
    invariant AllocInv(tid, addr, freeSpace, AtOrAfter);
  { 
    call found, addr := AllocAddrIfFree(tid, addr);
    if (found) {
      yield AllocInv(tid, addr, freeSpace, AtOrAfter);
      return;
    } 
    yield AllocInv(tid, addr, freeSpace, AtOrAfter);
  }
  assert false;
}
\end{verbatim}
\begin{verbatim}
procedure Free({:cnst "tid"} tid:int, addr:int)
  refines {:atomic} [Mem[addr] := true;]
{
  FreeAddr(tid, addr);  
  IncFreeSpace(); 
}
\end{verbatim}
\begin{verbatim}
AllocInv(tid, addr, freeSpace, AtOrAfter) = 
  0 <= freeSpace && lo <= addr <= hi &&
  #(AtOrAfter[lo],0,tid_max) + freeSpace == #(Mem,lo,hi) && 
  (forall u,v :: lo <= u <= v <= hi ==> 
         Subset(AtOrAfter[v], AtOrAfter[u])) &&
  (forall u :: 
         #(AtOrAfter[u],0,tid_max) <= #(Mem,u,hi) &&
         AtOrAfter[u][tid] <==> lo <= u && u <= addr)
\end{verbatim}
\end{small}
\caption{An example of multiple phases of refinement}
\label{fig:refTop}
\end{figure}


\begin{figure}
\begin{small}
\begin{verbatim}
procedure Reserve({:cnst "tid"} tid:int) 
  refines {:atomic} [assume freeSpace >= 1; 
                     freeSpace := freeSpace - 1;
                     AtOrAfter[tid][lo] := true;]
{
  while (true) {
    call tmp := ReadFreeSpace();
    if (tmp > 0) {
       call success := CAS_freeSpace(tmp,tmp-1);
       if (success)
         return; 
       yield;
    }
  }
}
\end{verbatim}
\begin{verbatim}
procedure IncFreeSpace() 
  refines {:left} [freeSpace := freeSpace + 1;]
{
  while (true) {
    call tmp := ReadFreeSpace();
    success := CAS_freeSpace(tmp, tmp+1)
    if (success)  
      return;
    yield;
  }
}
\end{verbatim}
\begin{verbatim}
procedure AllocAddrIfFree({:cnst "tid"} tid:int, addr:int) 
  returns res:bool
  refines {:atomic} [ res := false;
                      if (Mem[addr]) {
                         Mem[addr] := false; 
                         res := true;
                      } ]
                    
\end{verbatim}
\begin{verbatim}
procedure FreeAddr({:cnst "tid"} tid:int, addr:int)
  refines {:atomic} [Mem[addr] := true;]
\end{verbatim}
\end{small}
\caption{An example of multiple phases of refinement}
\label{fig:refinementBot}
\end{figure}

The \exC{Alloc} procedure is possibly blocking and returns when it
finds an address \exC{addr} such that \exC{Mem[addr]} is
\exC{free}. \exC{Free(addr)} simply frees the address
\exC{addr}. 
Before \exC{Alloc} scans the range of addresses
\exC{[lo,hi]}, it calls \exC{Reserve}, which continuously checks if
\exC{freeSpace > 0} and tries to atomically decrement \exC{freeSpace}
and reserves a \exC{free} address for later allocation by
\exC{Alloc}'s \exC{while} loop. It is non-trivial to verify that this
obviously-terminating \exC{while} loop succeeds in finding a
\exC{free} address. The variable \exC{freeSpace} keeps track of the
number of \exC{free} addresses that have not been reserved in this
manner. 

In this example, three descriptions of the program at different levels
of abstraction and atomicity are related by refinement. 
The bottom-level description consists of the entire program with all
variables present and no simplification due to abstract atomic
procedures. 

To obtain the middle-level description from the bottom-level
  one, we hide \exC{allocLock}. We verify that 
the calls to \exC{AllocAddrIfFree}, \exC{FreeAddr},
\exC{Reserve}, and
\exC{IncrementFreeSpace} can be replaced by their atomic action
specifications. 

The top-level representation only
consists of \exC{Alloc} and \exC{Free}'s atomic action
specifications. To verify \exC{Free}, we verify that \exC{IncrementFreeSpace}'s atomic
action specification is a left mover, we are able to show that \exC{Free} is
atomic and satisfies its atomic action specification at the next level. 
Verifying refinement and atomicity for \exC{Alloc} makes use
of the fact that \exC{Reserve} is atomic. To prove that \exC{Alloc}
satisfies its atomic action specification, we make use of an auxiliary
variable \exC{AtOrAfter}. \exC{AtOrAfter[u][tid] == true} iff thread
\exC{tid} has successfully completed executing \exC{Reserve} but has
not returned, and its local variable \exC{addr >= u}. We also make use
of the function \exC{\#Free} where \exC{\#Free[u,v]} returns the number
of addresses \exC{addr} in the interval \exC{[u,v]} such that
\exC{Mem[addr] == free}. 
\exC{Reserve}
establishes the following important facts when \exC{Alloc}'s
\exC{while} loop is about to be entered: \exC{AtOrAfter[lo][tid]} and 
\begin{verbatim}
  Size(AtOrAfter[lo]) + freeSpace == #Free[lo,hi] 
\end{verbatim}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "paper"
%%% End: