Quelle  Lock_Ticket.thy

(* Title:          Ticket 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>
*)

(* In the formal proof document, the Ticket Lock section starts with
the content of the helper Function_Supplementary, followed by the
actual definitions and RG theorems here. *)

subsection ‹Basic Definitions›

theory Lock_Ticket

imports
  RG_Annotated_Commands
  Function_Supplementary

begin

type_synonym thread_id = nat

definition positive_nats :: "nat set" where
  "positive_nats ≡ { n. 0 < n }"

text ‹The state of the Ticket Lock consists of three fields.›

record tktlock_state =
  now_serving :: "nat"
  next_ticket :: "nat"
  myticket :: "thread_id ==> nat"

text ‹Every thread locally stores a ticket number, and this collection of
  variables is modelled globally by the @{term myticket} function.

  Thread @{term i} joins the queue, it sets @{term ‹myticket i›} to be
  value @{term ‹next_ticket›}, and atomically increments @{term next_ticket};
  corresponds to the atomic Fetch-And-Add instruction, which is supported
  most computer systems.
 
  @{term i} then waits until the @{term now_serving} value becomes
  to its own ticket number @{term ‹myticket i›}.
 
  Thread @{term i} leaves the queue, it increments @{term now_serving}.

  steps correspond to the following code for Acquire and Release.
  that we use forward function composition to model the Fetch-And-Add
 .

 {theory_text[display = true] ‹
 acquire ≡ ((myticket i := next_ticket) ∘>
 (next_ticket := next_ticket + 1));
 WHILE now_serving ≠ myticket i DO SKIP OD)

 release ≡ now_serving := now_serving + 1
 ›}

 , Thread @{term i} is in the queue if and only if
 {theory_text ‹now_serving ≤ myticket i›}
  is at the head if and only if
 {theory_text ‹now_serving = myticket i›}.›

(*------------------------------------------------------------------*)
text ‹Now, in the initial state, every thread holds the number 0 as
  ticket, and both @{term now_serving} and @{term next_ticket} are
  to 1.›

abbreviation tktlock_init :: "tktlock_state set" where
  "tktlock_init ≡ { 🍋myticket = (λj. 0) ∧
    🍋now_serving = 1 ∧ 🍋next_ticket = 1 }"

text ‹We further define a shorthand for describing the set of ticket
  use; i.e.\ those numbers from @{term now_serving} up to, but not
  @{term next_ticket}. This shorthand will later be used in
  invariant.›

abbreviation tktlock_contending_set :: "tktlock_state ==> thread_id set" where
  "tktlock_contending_set s ≡ { j. now_serving s ≤ myticket s j }"

(*------------------------------------------------------------------*)
text ‹We now formalise the invariant of the Ticket Lock.›

abbreviation tktlock_inv :: "tktlock_state set" where
  "tktlock_inv ≡ { 🍋now_serving ≤ 🍋next_ticket ∧
    1 ≤ 🍋now_serving ∧
    (∀ j. 🍋myticket j < 🍋next_ticket) ∧
    bij_betw 🍋myticket 🍋tktlock_contending_set {🍋now_serving ..< 🍋next_ticket} ∧
    inj_img 🍋myticket positive_nats }"

text ‹The first three clauses are basic inequalities.

  penultimate clause stipulates that the function @{term myticket}
  every valid state is bijective between the set of queuing/contending
  (those threads whose tickets are not smaller than @{term now_serving})
  .

  final clause ensures that the function @{term myticket} is injective
  0 is excluded from its codomain. In other words, all threads, whose
  are non-zero, hold unique tickets.›

(*------------------------------------------------------------------*)
text ‹As for the contract, the first clause ensures that the local
  @{term ‹myticket i›} does not change. Meanwhile, the global
  @{term next_ticket} and @{term now_serving} must not decrease,
  stipulated by the second and third clauses of the contract.

  last two clauses of the contract correspond to the two clauses of
  contract of the Abstract Queue Lock, where
 {theory_text ‹i ∈ set queue›} and @{theory_text ‹at_head i queue›}
  the Abstract Queue Lock respectively translate to
 {theory_text ‹now_serving ≤ myticket i›} and
 {theory_text ‹now_serving = myticket i›} under the Ticket Lock.›

abbreviation tktlock_contract :: "thread_id ==> tktlock_state rel" where
  "tktlock_contract i ≡ { ♂myticket i = ♀myticket i ∧
    ♂next_ticket ≤ ♀next_ticket ∧
    ♂now_serving ≤ ♀now_serving ∧
    (♂now_serving ≤ ♂myticket i ⟷ ♀now_serving ≤ ♀myticket i) ∧
    (♂now_serving = ♂myticket i ⟶ ♀now_serving = ♀myticket i) }"

(*------------------------------------------------------------------*)
text ‹We further state and prove some helper lemmas that will be used later.›

lemma tktlock_contending_set_rewrite:
  "tktlock_contending_set s ∪ {i} = {🍋(≠) i ⟶ now_serving s ≤ 🍋(myticket s)}" 
  by fastforce

lemma tktlock_used_tickets_rewrite:
  assumes "now_serving s ≤ next_ticket s"
    shows "{now_serving s ..< next_ticket s} ∪ {next_ticket s}
         = {now_serving s ..< Suc (next_ticket s)}"
  by (fastforce simp: assms atLeastLessThanSuc)

lemma tktlock_enqueue_bij:
  assumes "myticket s i < now_serving s"
      and "bij_betw (myticket s) (tktlock_contending_set s) {now_serving s ..< next_ticket s}"
    shows "bij_betw ( (myticket s)(i := next_ticket s) )
                    ( tktlock_contending_set s ∪ {i} )
                    ( {now_serving s ..< next_ticket s} ∪ {next_ticket s} )"
  apply (rule bij_extension)
  using assms by fastforce+

lemma tktlock_enqueue_inj:
  assumes "s ∈ tktlock_inv"
  shows "inj_img ((myticket s)(i := next_ticket s)) positive_nats"
  apply(subst inj_img_fun_upd_notin)
  using assms by (fastforce simp: nat_less_le)+

method clarsimp_seq = clarsimp, standard, clarsimp

(*------------------------------------------------------------------*)
subsection ‹RG Theorems›

text ‹The RG sentence of the first instruction of Acquire.›

lemma tktlock_acq1:
  "rely: tktlock_contract i guar: for_others tktlock_contract i
   inv: tktlock_inv anno_code:
   { { 🍋myticket i < 🍋now_serving } }
     BasicAnno ((🍋myticket[i] ← 🍋next_ticket) ∘>
                (🍋next_ticket ← 🍋next_ticket + 1))
   { { 🍋now_serving ≤ 🍋myticket i } }"
proof method_anno_ultimate
  case est_guar
  thus ?case
    apply clarsimp_seq
     apply (fastforce simp: less_Suc_eq)
    using tktlock_contending_set_rewrite tktlock_enqueue_bij 
    by (fastforce simp: atLeastLessThanSuc tktlock_enqueue_inj)
next
  case est_post
  thus ?case
    apply clarsimp_seq
     apply (fastforce simp: less_Suc_eq)
    using tktlock_contending_set_rewrite tktlock_enqueue_bij 
    by (fastforce simp: atLeastLessThanSuc tktlock_enqueue_inj) 
qed (fastforce)+

text ‹A helper lemma for the Release procedure.›

lemma tktlock_rel_helper:
  assumes inv1: "now_serving s = myticket s i"
      and inv2: "myticket s i ≤ next_ticket s"
      and inv3: "Suc 0 ≤ myticket s i"
      and inv4: "∀j. myticket s j < next_ticket s"
      and bij_old: "bij_betw (myticket s)
                             {myticket s i ≤ 🍋(myticket s)}
                             {myticket s i ..< next_ticket s}"
    shows "bij_betw (myticket s)
                    {Suc (myticket s i) ≤ 🍋(myticket s)}
                    {Suc (myticket s i) ..< next_ticket s}"
proof -
  have thread_rewrite:
    "{ Suc (myticket s i) ≤ 🍋(myticket s)} = {j. myticket s i ≤ myticket s j} - {i}"
    apply (subst set_remove_one_element[where B="{j. Suc (myticket s i) ≤ myticket s j}"]; clarsimp)
    by(metis CollectI Suc_leI assms(5) bij_betw_def inj_onD order_le_imp_less_or_eq)
  have ticket_rewrite: 
    "{Suc (myticket s i) ..< next_ticket s} = {myticket s i ..< next_ticket s} - {myticket s i}"
    by fastforce
  have "bij_betw (myticket s)
                 ( {j. myticket s i ≤ myticket s j} - {i} )
                 ( {myticket s i ..< next_ticket s} - {myticket s i} )"
    by (rule bij_remove_one; clarsimp simp: bij_old)
  thus ?thesis
    by (clarsimp simp: thread_rewrite ticket_rewrite)
qed

text ‹The RG sentence for the Release procedure.›

lemma tktlock_rel:
  "rely: tktlock_contract i
   guar: for_others tktlock_contract i
   inv: tktlock_inv

   code: { { 🍋now_serving = 🍋myticket i } }
           🍋now_serving := 🍋now_serving + 1
         { { 🍋myticket i < 🍋now_serving } }"
proof method_basic_inv
  case est_inv
  thus ?case
    by (clarsimp, fastforce simp: Suc_le_eq intro!: tktlock_rel_helper)
next
  case est_guar
  thus ?case
    by (clarsimp, fastforce simp: less_eq_Suc_le nat_less_le positive_nats_def inj_img_def)
qed (fastforce)+

text ‹The RG sentence for a thread that performs Acquire and then Release.›

lemma tktlock_local:
 "rely: tktlock_contract i guar: for_others tktlock_contract i
  inv: tktlock_inv anno_code:

   { { 🍋myticket i < 🍋now_serving } }
   BasicAnno ((🍋myticket[i] ← 🍋next_ticket) ∘>
              (🍋next_ticket ← 🍋next_ticket + 1)) .;
   { { 🍋now_serving ≤ 🍋myticket i } }
   NoAnno (WHILE 🍋now_serving ≠ 🍋myticket i DO SKIP OD) .;
   { { 🍋now_serving = 🍋myticket i } }
   NoAnno (🍋now_serving := 🍋now_serving + 1)
   { { 🍋myticket i < 🍋now_serving } }"
  apply (method_anno_ultimate, goal_cases)
    using tktlock_acq1 apply fastforce 
   apply (clarsimp, method_spinloop; fastforce)
  using tktlock_rel by fastforce

text ‹The RG sentence for a thread that repeatedly performs Acquire
  then Release in an infinite loop.›

lemma tktlock_local_loop:
 "rely: tktlock_contract i guar: for_others tktlock_contract i
  inv: tktlock_inv anno_code:

   { { 🍋myticket i < 🍋now_serving } }
   WHILEa True DO
    {stable_guard: { 🍋myticket i < 🍋now_serving } }
     BasicAnno ((🍋myticket[i] ← 🍋next_ticket) ∘>
                (🍋next_ticket ← 🍋next_ticket + 1)) .;
     { { 🍋now_serving ≤ 🍋myticket i } }
     NoAnno (WHILE 🍋now_serving ≠ 🍋myticket i DO SKIP OD) .;
     { { 🍋now_serving = 🍋myticket i } }
     NoAnno (🍋now_serving := 🍋now_serving + 1)
   OD
   { { 🍋myticket i < 🍋now_serving } }"
proof method_anno_ultimate
  case body
  thus ?case 
    using tktlock_local by (fastforce simp: Int_commute)
qed (fastforce)+

text ‹The global RG sentence for a set of threads, each of which
  performs Acquire and then Release in an infinite loop.›

theorem tktlock_global:
  assumes "0 < n"
    shows "annotated
  global_init: { 🍋now_serving = 1 ∧ 🍋next_ticket = 1 ∧ 🍋myticket = (λj. 0) }
  global_rely: Id
    ∥ i < n @

  { { 🍋myticket i < 🍋now_serving }, tktlock_contract i }
  WHILEa True DO
    {stable_guard: { 🍋myticket i < 🍋now_serving } }
    BasicAnno ((🍋myticket[i] ← 🍋next_ticket) ∘>
               (🍋next_ticket ← 🍋next_ticket + 1)) .;
    { { 🍋now_serving ≤ 🍋myticket i } }
    NoAnno (WHILE 🍋now_serving ≠ 🍋myticket i DO SKIP OD) .;
    { { 🍋now_serving = 🍋myticket i } }
    NoAnno (🍋now_serving := 🍋now_serving + 1)
  OD

  // tktlock_inv { for_others tktlock_contract i, {} }
  global_guar: UNIV
  global_post: {}"
proof method_anno_ultimate
  case (local_sat i)
  thus ?case using tktlock_local_loop by fastforce
next
  case (pre i)
  thus ?case
    using bij_betwI' inj_img_def positive_nats_def by fastforce
next
  case (guar_imp_rely i j)
  thus ?case   
    by auto[1]
qed (fastforce simp: assms)+

end