counter_lock.mlw

(* Implementation of concurrent counter, assuming atomic updates are not available.
   Threads have a local copy of the counter; access to to the shared counter 
   variable is controled using a lock. 
   We prove that this refines the abstract counter spec. 
 *)


module CounterImpl

  use counter.Counter

  type state = Zero | One | Two | Three | Four
  type lock = Unlocked | Locked thread

  (* System configurations
   *)
  type world = { pcc : map thread state ;
       	       	 x : int ;
		 y : map thread int ;
		 lock :lock }
  

  (* Refinement mapping: Inc state is mapped to Start at abstract level
   *) 
  let function refn (w:world) : Counter.world
  = let pc' (t:thread) = match w.pcc[t] with
                         | Three -> Counter.Done
                         | Four -> Counter.Done
			 | _ -> Counter.Start
			 end
    in { pc = pc' ; counter = w.x  }


  (* Inductive invariant 
     required to prove refinement conditions
   *)
  (* predicate inv (w:world) =  *)
  (*   forall t :thread. w.lock = Locked t -> w.y[t] = w.x *)

  predicate inv (w:world) =
    (forall t :thread. w.pcc[t]<>Zero /\ w.pcc[t]<>Four -> w.lock = Locked t)
     /\
    (forall t :thread. w.pcc[t] = Two -> w.y[t] = w.x)


  (* System INIT 
   *)
  predicate initWorld_p (w:world) =
    w.pcc = const Zero /\ w.x = 0 /\ w.y = const 0 /\ w.lock = Unlocked

  let ghost predicate initWorld (w:world)
    ensures { result -> inv w }
    ensures { result -> Counter.initWorld (refn w) }
  = initWorld_p w 


  (* System actions
   *)
  predicate step_Zero_enbld (w:world) (t:thread) = 
    w.pcc[t] = Zero /\ w.lock = Unlocked 

  let ghost function step_Zero (w:world) (t:thread) : world
    requires { step_Zero_enbld w t }
    ensures  { inv w -> inv result }
    ensures  { inv w -> refn result = refn w \/ Counter.stepind (refn w) (refn result) }
  = { pcc = set (w.pcc) t One ;
      x = w.x ;
      y = w.y ;
      lock = Locked t }


  predicate step_One_enbld (w:world) (t:thread) = 
    w.pcc[t] = One

  let ghost function step_One (w:world) (t:thread) : world
    requires { step_One_enbld w t }
    ensures  { inv w -> inv result }
    ensures  { inv w -> refn result = refn w \/ Counter.stepind (refn w) (refn result) }
  = { pcc = set (w.pcc) t Two ;
      x = w.x ;
      y = set (w.y) t w.x ;
      lock = w.lock }


  predicate step_Two_enbld (w:world) (t:thread) = 
    w.pcc[t] = Two

  let ghost function step_Two (w:world) (t:thread) : world
    requires { step_Two_enbld w t }
    ensures  { inv w -> inv result }
    ensures  { inv w -> refn result = refn w \/ Counter.stepind (refn w) (refn result) }
  = { pcc = set (w.pcc) t Three ;
      x = w.y[t] +1 ;
      y = w.y ;
      lock = w.lock }


  predicate step_Three_enbld (w:world) (t:thread) = 
    w.pcc[t] = Three

  let ghost function step_Three (w:world) (t:thread) : world
    requires { step_Three_enbld w t }
    ensures  { inv w -> inv result }
    ensures  { inv w -> refn result = refn w \/ Counter.stepind (refn w) (refn result) }
  = { pcc = set (w.pcc) t Four ;
      x = w.x ;
      y = w.y ;
      lock = Unlocked }


  (* Transition relation
   *)
  inductive stepind world world =
  | step_Zero : forall w :world, t :thread.
      step_Zero_enbld w t -> stepind w  (step_Zero w t )
  | step_One : forall w :world, t :thread.
      step_One_enbld w t -> stepind w  (step_One w t )
  | step_Two : forall w :world, t :thread.
      step_Two_enbld w t -> stepind w  (step_Two w t )
  | step_Three : forall w :world, t :thread.
      step_Three_enbld w t -> stepind w  (step_Three w t )

  let ghost predicate step (w1:world) (w2:world) = stepind w1 w2 


  (* Proof of refinement 
   *)
  clone refinement.Refinement with
    type worldC=world, type worldA=Counter.world, val refn,
    predicate invC=inv, predicate invA=Counter.inv,
    val initWorldC=initWorld, val initWorldA=Counter.initWorld,
    val stepC=step, val stepA=Counter.step

   (* the abstract invariant holds in all concrete reachable configurations
    *)
  lemma safety_by_refinement : forall w :world. reachableC w -> reachableA (refn w)


end