Theory Lock_Ticket
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
local variables is modelled globally by the @{term myticket} function.
When Thread @{term i} joins the queue, it sets @{term ‹myticket i›} to be
the value @{term ‹next_ticket›}, and atomically increments @{term next_ticket};
this corresponds to the atomic Fetch-And-Add instruction, which is supported
on most computer systems.
%
Thread @{term i} then waits until the @{term now_serving} value becomes
equal to its own ticket number @{term ‹myticket i›}.
%
When Thread @{term i} leaves the queue, it increments @{term now_serving}.
These steps correspond to the following code for Acquire and Release.
Note that we use forward function composition to model the Fetch-And-Add
instruction.
@{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
›}
Conceptually, Thread @{term i} is in the queue if and only if
@{theory_text ‹now_serving ≤ myticket i›}
and 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
its ticket, and both @{term now_serving} and @{term next_ticket} are
set 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
in use; i.e.\ those numbers from @{term now_serving} up to, but not
including @{term next_ticket}. This shorthand will later be used in
the 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.
The penultimate clause stipulates that the function @{term myticket}
of every valid state is bijective between the set of queuing/contending
threads (those threads whose tickets are not smaller than @{term now_serving})
and .
The final clause ensures that the function @{term myticket} is injective
when 0 is excluded from its codomain. In other words, all threads, whose
tickets are non-zero, hold unique tickets.›
text ‹As for the contract, the first clause ensures that the local
variable @{term ‹myticket i›} does not change. Meanwhile, the global
variables @{term next_ticket} and @{term now_serving} must not decrease,
as stipulated by the second and third clauses of the contract.
The last two clauses of the contract correspond to the two clauses of
the contract of the Abstract Queue Lock, where
@{theory_text ‹i ∈ set queue›} and @{theory_text ‹at_head i queue›}
under 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
and 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
repeatedly 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