Theory Lock_Abstract_Queue

(* Title:      	   Abstract Queue Lock
   Author(s):     Robert Colvin, Scott Heiner, Peter Hoefner, Roger Su
   License:       BSD 2-Clause
   Maintainer(s): Roger Su <roger.c.su@proton.me>
                  Peter Hoefner <peter@hoefner-online.de>
*)

section ‹Abstract Queue Lock›

theory Lock_Abstract_Queue

imports
  RG_Annotated_Commands

begin

text ‹We identify each thread by a natural number.›

type_synonym thread_id = nat

text ‹The state of the Abstract Queue Lock consists of one single
field, which is the list of threads.›

record queue_lock = queue :: "thread_id list"

text ‹The following abbreviation describes when an object is at the
head of a list. Note that both clauses are needed to characterise the
predicate faithfully, because the term @{term ‹x = hd xs›} (i.e.\
@{term x} is the head of @{term xs}) does not imply that @{term ‹x ∈ set xs›}.›

abbreviation at_head :: "'a ⇒ 'a list ⇒ bool" where
  "at_head x xs ≡ xs ≠ [] ∧ x = hd xs"

text ‹The contract of the Abstract Queue Lock consists of two clauses.
The first states that a thread cannot be added to or removed from the
queue by its environment. The second states that the head of the queue
remains at the head after any environment-step.›

abbreviation queue_contract :: "thread_id ⇒ queue_lock rel" where
  "queue_contract i ≡ ⦃
    (i ∈ set ºqueue ⟷ i ∈ set ªqueue) ∧
    (at_head i ºqueue ⟶ at_head i ªqueue) ⦄"

text ‹The RG sentence of the Release procedure is made into a separate
lemma below.›

lemma qlock_rel:
 "rely: queue_contract t     guar: for_others queue_contract t
  inv:  ⦃ distinct ´queue ⦄  code:
    { ⦃ at_head t ´queue ⦄ }
  ´queue := tl ´queue
    { ⦃ t ∉ set ´queue ⦄ }"
proof method_basic_inv
  case est_guar
  then show ?case
    apply clarsimp
    by (metis hd_Cons_tl in_set_member member_rec(1))
next
  case est_post
  then show ?case
    apply clarsimp
    by (metis distinct.simps(2) list.collapse)
qed (simp_all add: distinct_tl)

text ‹The correctness of the Abstract Queue Lock is expressed by the
following RG sentence, which describes a closed system of @{term n} 
threads, each repeatedly calls Acquire and then Release in an infinite
loop. We omit the critical section between Acquire and Release, as it
does not access the lock.

The Acquire procedure consists of two steps: enqueuing and spinning.
The Release procedure consists of only the dequeuing step.

Each thread can only be in the queue at most once, so the invariant
requires the queue to be distinct.

The queue is initially empty; hence the global precondition.
Being a closed system, there is no external actor, so the rely is the
identity relation, and the guarantee is the universal relation.
The system executes continuously, as the outer infinite loop never
terminates; hence, the global postcondition is the empty set.
›

theorem qlock_global:
  assumes "0 < n"
  shows "annotated
  global_init: ⦃ ´queue = [] ⦄  global_rely: Id
    ∥ i < n @
  { ⦃ i ∉ set ´queue ⦄, queue_contract i }

  WHILEa True DO
    {stable_guard: ⦃ i ∉ set ´queue ⦄ }
    NoAnno (´queue := ´queue @ [i]) .;
    { ⦃ i ∈ set ´queue ⦄ }
    NoAnno (WHILE hd ´queue ≠ i DO SKIP OD) .;
    { ⦃ at_head i ´queue ⦄}
    NoAnno (´queue := tl ´queue)
  OD

  ⫽ ⦃ distinct ´queue ⦄ { for_others queue_contract i, {} }
  global_guar: UNIV  global_post: {}"
  apply rg_proof_expand
     apply (method_basic; fastforce)
    apply (method_spinloop; fastforce)
   using qlock_rel apply fastforce
  using assms by fastforce

end