Quelle  OG_Examples.thy

section ‹Examples›

theory OG_Examples imports OG_Syntax begin

subsection ‹Mutual Exclusion›

subsubsection ‹Peterson's Algorithm I›

text ‹Eike Best. "Semantics of Sequential and Parallel Programs", page 217.›

record Petersons_mutex_1 =
 pr1 :: nat
 pr2 :: nat
 in1 :: bool
 in2 :: bool
 hold :: nat

lemma Petersons_mutex_1:
  "∥- {🍋pr1=0 ∧ ¬🍋in1 ∧ 🍋pr2=0 ∧ ¬🍋in2 }
  COBEGIN {🍋pr1=0 ∧ ¬🍋in1}
  WHILE True INV {🍋pr1=0 ∧ ¬🍋in1}
  DO
  {🍋pr1=0 ∧ ¬🍋in1} ⟨ 🍋in1:=True,,🍋pr1:=1 ⟩;;
  {🍋pr1=1 ∧ 🍋in1} ⟨ 🍋hold:=1,,🍋pr1:=2 ⟩;;
  {🍋pr1=2 ∧ 🍋in1 ∧ (🍋hold=1 ∨ 🍋hold=2 ∧ 🍋pr2=2)}
  AWAIT (¬🍋in2 ∨ ¬(🍋hold=1)) THEN 🍋pr1:=3 END;;
  {🍋pr1=3 ∧ 🍋in1 ∧ (🍋hold=1 ∨ 🍋hold=2 ∧ 🍋pr2=2)}
   ⟨🍋in1:=False,,🍋pr1:=0⟩
  OD {🍋pr1=0 ∧ ¬🍋in1}
  ∥
  {🍋pr2=0 ∧ ¬🍋in2}
  WHILE True INV {🍋pr2=0 ∧ ¬🍋in2}
  DO
  {🍋pr2=0 ∧ ¬🍋in2} ⟨ 🍋in2:=True,,🍋pr2:=1 ⟩;;
  {🍋pr2=1 ∧ 🍋in2} ⟨ 🍋hold:=2,,🍋pr2:=2 ⟩;;
  {🍋pr2=2 ∧ 🍋in2 ∧ (🍋hold=2 ∨ (🍋hold=1 ∧ 🍋pr1=2))}
  AWAIT (¬🍋in1 ∨ ¬(🍋hold=2)) THEN 🍋pr2:=3 END;;
  {🍋pr2=3 ∧ 🍋in2 ∧ (🍋hold=2 ∨ (🍋hold=1 ∧ 🍋pr1=2))}
    ⟨🍋in2:=False,,🍋pr2:=0⟩
  OD {🍋pr2=0 ∧ ¬🍋in2}
  COEND
  {🍋pr1=0 ∧ ¬🍋in1 ∧ 🍋pr2=0 ∧ ¬🍋in2}"
apply oghoare
🍋 ‹104 verification conditions.›
apply auto
done

subsubsection ‹Peterson's Algorithm II: A Busy Wait Solution›

text ‹Apt and Olderog. "Verification of sequential and concurrent Programs", page 282.›

record Busy_wait_mutex =
 flag1 :: bool
 flag2 :: bool
 turn  :: nat
 after1 :: bool
 after2 :: bool

lemma Busy_wait_mutex:
 "∥- {True}
  🍋flag1:=False,, 🍋flag2:=False,,
  COBEGIN {¬🍋flag1}
        WHILE True
        INV {¬🍋flag1}
        DO {¬🍋flag1} ⟨ 🍋flag1:=True,,🍋after1:=False ⟩;;
           {🍋flag1 ∧ ¬🍋after1} ⟨ 🍋turn:=1,,🍋after1:=True ⟩;;
           {🍋flag1 ∧ 🍋after1 ∧ (🍋turn=1 ∨ 🍋turn=2)}
            WHILE ¬(🍋flag2 ⟶ 🍋turn=2)
            INV {🍋flag1 ∧ 🍋after1 ∧ (🍋turn=1 ∨ 🍋turn=2)}
            DO {🍋flag1 ∧ 🍋after1 ∧ (🍋turn=1 ∨ 🍋turn=2)} SKIP OD;;
           {🍋flag1 ∧ 🍋after1 ∧ (🍋flag2 ∧ 🍋after2 ⟶ 🍋turn=2)}
            🍋flag1:=False
        OD
       {False}
  ∥
     {¬🍋flag2}
        WHILE True
        INV {¬🍋flag2}
        DO {¬🍋flag2} ⟨ 🍋flag2:=True,,🍋after2:=False ⟩;;
           {🍋flag2 ∧ ¬🍋after2} ⟨ 🍋turn:=2,,🍋after2:=True ⟩;;
           {🍋flag2 ∧ 🍋after2 ∧ (🍋turn=1 ∨ 🍋turn=2)}
            WHILE ¬(🍋flag1 ⟶ 🍋turn=1)
            INV {🍋flag2 ∧ 🍋after2 ∧ (🍋turn=1 ∨ 🍋turn=2)}
            DO {🍋flag2 ∧ 🍋after2 ∧ (🍋turn=1 ∨ 🍋turn=2)} SKIP OD;;
           {🍋flag2 ∧ 🍋after2 ∧ (🍋flag1 ∧ 🍋after1 ⟶ 🍋turn=1)}
            🍋flag2:=False
        OD
       {False}
  COEND
  {False}"
apply oghoare
🍋 ‹122 vc›
apply auto
done

subsubsection ‹Peterson's Algorithm III: A Solution using Semaphores›

record  Semaphores_mutex =
 out :: bool
 who :: nat

lemma Semaphores_mutex:
 "∥- {i≠j}
  🍋out:=True ,,
  COBEGIN {i≠j}
       WHILE True INV {i≠j}
       DO {i≠j} AWAIT 🍋out THEN 🍋out:=False,, 🍋who:=i END;;
          {¬🍋out ∧ 🍋who=i ∧ i≠j} 🍋out:=True OD
       {False}
  ∥
       {i≠j}
       WHILE True INV {i≠j}
       DO {i≠j} AWAIT 🍋out THEN 🍋out:=False,,🍋who:=j END;;
          {¬🍋out ∧ 🍋who=j ∧ i≠j} 🍋out:=True OD
       {False}
  COEND
  {False}"
apply oghoare
🍋 ‹38 vc›
apply auto
done

subsubsection ‹Peterson's Algorithm III: Parameterized version:›

lemma Semaphores_parameterized_mutex:
 "0==> ∥- {True}
  🍋out:=True ,,
 COBEGIN
  SCHEME [0≤ i< n]
    {True}
     WHILE True INV {True}
      DO {True} AWAIT 🍋out THEN 🍋out:=False,, 🍋who:=i END;;
         {¬🍋out ∧ 🍋who=i} 🍋out:=True OD
    {False}
 COEND
  {False}"
apply oghoare
🍋 ‹20 vc›
apply auto
done

subsubsection‹The Ticket Algorithm›

record Ticket_mutex =
 num :: nat
 nextv :: nat
 turn :: "nat list"
 index :: nat

lemma Ticket_mutex:
 "[ 0«n=length 🍋turn ∧ 0<🍋nextv ∧ (∀k l. k∧ l∧ k≠l
    ⟶ 🍋turn!k < 🍋num ∧ (🍋turn!k =0 ∨ 🍋turn!k≠🍋turn!l))¬ ]
   ==> ∥- {n=length 🍋turn}
   🍋index:= 0,,
   WHILE 🍋index < n INV {n=length 🍋turn ∧ (∀i<🍋index. 🍋turn!i=0)}
    DO 🍋turn:= 🍋turn[🍋index:=0],, 🍋index:=🍋index +1 OD,,
  🍋num:=1 ,, 🍋nextv:=1 ,,
 COBEGIN
  SCHEME [0≤ i< n]
    {🍋I}
     WHILE True INV {🍋I}
      DO {🍋I} ⟨ 🍋turn :=🍋turn[i:=🍋num],, 🍋num:=🍋num+1 ⟩;;
         {🍋I} WAIT 🍋turn!i=🍋nextv END;;
         {🍋I ∧ 🍋turn!i=🍋nextv} 🍋nextv:=🍋nextv+1
      OD
    {False}
 COEND
  {False}"
apply oghoare
🍋 ‹35 vc›
apply simp_all
🍋 ‹16 vc›
apply(tactic ‹ALLGOALS (clarify_tac 🍋)›)
🍋 ‹11 vc›
apply simp_all
apply(tactic ‹ALLGOALS (clarify_tac 🍋)›)
🍋 ‹10 subgoals left›
apply(erule less_SucE)
 apply simp
apply simp
🍋 ‹9 subgoals left›
apply(case_tac "i=k")
 apply force
apply simp
apply(case_tac "i=l")
 apply force
apply force
🍋 ‹8 subgoals left›
prefer 8
apply force
apply force
🍋 ‹6 subgoals left›
prefer 6
apply(erule_tac x=j in allE)
apply fastforce
🍋 ‹5 subgoals left›
prefer 5
apply(case_tac [!] "j=k")
🍋 ‹10 subgoals left›
apply simp_all
apply(erule_tac x=k in allE)
apply force
🍋 ‹9 subgoals left›
apply(case_tac "j=l")
 apply simp
 apply(erule_tac x=k in allE)
 apply(erule_tac x=k in allE)
 apply(erule_tac x=l in allE)
 apply force
apply(erule_tac x=k in allE)
apply(erule_tac x=k in allE)
apply(erule_tac x=l in allE)
apply force
🍋 ‹8 subgoals left›
apply force
apply(case_tac "j=l")
 apply simp
apply(erule_tac x=k in allE)
apply(erule_tac x=l in allE)
apply force
apply force
apply force
🍋 ‹5 subgoals left›
apply(erule_tac x=k in allE)
apply(erule_tac x=l in allE)
apply(case_tac "j=l")
 apply force
apply force
apply force
🍋 ‹3 subgoals left›
apply(erule_tac x=k in allE)
apply(erule_tac x=l in allE)
apply(case_tac "j=l")
 apply force
apply force
apply force
🍋 ‹1 subgoals left›
apply(erule_tac x=k in allE)
apply(erule_tac x=l in allE)
apply(case_tac "j=l")
 apply force
apply force
done

subsection‹Parallel Zero Search›

text ‹Synchronized Zero Search. Zero-6›

text ‹Apt and Olderog. "Verification of sequential and concurrent Programs" page 294:›

record Zero_search =
   turn :: nat
   found :: bool
   x :: nat
   y :: nat

lemma Zero_search:
  "[I1= « a≤🍋x ∧ (🍋found ⟶ (a<🍋x ∧ f(🍋x)=0) ∨ (🍋y≤a ∧ f(🍋y)=0))
      ∧ (¬🍋found ∧ a<🍋 x ⟶ f(🍋x)≠0) ¬ ;
    I2= «🍋y≤a+1 ∧ (🍋found ⟶ (a<🍋x ∧ f(🍋x)=0) ∨ (🍋y≤a ∧ f(🍋y)=0))
      ∧ (¬🍋found ∧ 🍋y≤a ⟶ f(🍋y)≠0) ¬ ] ==>
  ∥- {∃ u. f(u)=0}
  🍋turn:=1,, 🍋found:= False,,
  🍋x:=a,, 🍋y:=a+1 ,,
  COBEGIN {🍋I1}
       WHILE ¬🍋found
       INV {🍋I1}
       DO {a≤🍋x ∧ (🍋found ⟶ 🍋y≤a ∧ f(🍋y)=0) ∧ (a<🍋x ⟶ f(🍋x)≠0)}
          WAIT 🍋turn=1 END;;
          {a≤🍋x ∧ (🍋found ⟶ 🍋y≤a ∧ f(🍋y)=0) ∧ (a<🍋x ⟶ f(🍋x)≠0)}
          🍋turn:=2;;
          {a≤🍋x ∧ (🍋found ⟶ 🍋y≤a ∧ f(🍋y)=0) ∧ (a<🍋x ⟶ f(🍋x)≠0)}
          ⟨ 🍋x:=🍋x+1,,
            IF f(🍋x)=0 THEN 🍋found:=True ELSE SKIP FI⟩
       OD;;
       {🍋I1 ∧ 🍋found}
       🍋turn:=2
       {🍋I1 ∧ 🍋found}
  ∥
      {🍋I2}
       WHILE ¬🍋found
       INV {🍋I2}
       DO {🍋y≤a+1 ∧ (🍋found ⟶ a<🍋x ∧ f(🍋x)=0) ∧ (🍋y≤a ⟶ f(🍋y)≠0)}
          WAIT 🍋turn=2 END;;
          {🍋y≤a+1 ∧ (🍋found ⟶ a<🍋x ∧ f(🍋x)=0) ∧ (🍋y≤a ⟶ f(🍋y)≠0)}
          🍋turn:=1;;
          {🍋y≤a+1 ∧ (🍋found ⟶ a<🍋x ∧ f(🍋x)=0) ∧ (🍋y≤a ⟶ f(🍋y)≠0)}
          ⟨ 🍋y:=(🍋y - 1),,
            IF f(🍋y)=0 THEN 🍋found:=True ELSE SKIP FI⟩
       OD;;
       {🍋I2 ∧ 🍋found}
       🍋turn:=1
       {🍋I2 ∧ 🍋found}
  COEND
  {f(🍋x)=0 ∨ f(🍋y)=0}"
apply oghoare
🍋 ‹98 verification conditions›
apply auto
🍋 ‹auto takes about 3 minutes !!›
done

text ‹Easier Version: without AWAIT. Apt and Olderog. page 256:›

lemma Zero_Search_2:
"[I1=« a≤🍋x ∧ (🍋found ⟶ (a<🍋x ∧ f(🍋x)=0) ∨ (🍋y≤a ∧ f(🍋y)=0))
    ∧ (¬🍋found ∧ a<🍋x ⟶ f(🍋x)≠0)¬;
 I2= «🍋y≤a+1 ∧ (🍋found ⟶ (a<🍋x ∧ f(🍋x)=0) ∨ (🍋y≤a ∧ f(🍋y)=0))
    ∧ (¬🍋found ∧ 🍋y≤a ⟶ f(🍋y)≠0)¬] ==>
  ∥- {∃u. f(u)=0}
  🍋found:= False,,
  🍋x:=a,, 🍋y:=a+1,,
  COBEGIN {🍋I1}
       WHILE ¬🍋found
       INV {🍋I1}
       DO {a≤🍋x ∧ (🍋found ⟶ 🍋y≤a ∧ f(🍋y)=0) ∧ (a<🍋x ⟶ f(🍋x)≠0)}
          ⟨ 🍋x:=🍋x+1,,IF f(🍋x)=0 THEN 🍋found:=True ELSE SKIP FI⟩
       OD
       {🍋I1 ∧ 🍋found}
  ∥
      {🍋I2}
       WHILE ¬🍋found
       INV {🍋I2}
       DO {🍋y≤a+1 ∧ (🍋found ⟶ a<🍋x ∧ f(🍋x)=0) ∧ (🍋y≤a ⟶ f(🍋y)≠0)}
          ⟨ 🍋y:=(🍋y - 1),,IF f(🍋y)=0 THEN 🍋found:=True ELSE SKIP FI⟩
       OD
       {🍋I2 ∧ 🍋found}
  COEND
  {f(🍋x)=0 ∨ f(🍋y)=0}"
apply oghoare
🍋 ‹20 vc›
apply auto
🍋 ‹auto takes aprox. 2 minutes.›
done

subsection ‹Producer/Consumer›

subsubsection ‹Previous lemmas›

lemma nat_lemma2: "[ b = m*(n::nat) + t; a = s*n + u; t=u; b-a < n ] ==> m ≤ s"
proof -
  assume "b = m*(n::nat) + t" "a = s*n + u" "t=u"
  hence "(m - s) * n = b - a" by (simp add: diff_mult_distrib)
  also assume "… < n"
  finally have "m - s < 1" by simp
  thus ?thesis by arith
qed

lemma mod_lemma: "[ (c::nat) ≤ a; a < b; b - c < n ] ==> b mod n ≠ a mod n"
apply(subgoal_tac "b=b div n*n + b mod n" )
 prefer 2  apply (simp add: div_mult_mod_eq [symmetric])
apply(subgoal_tac "a=a div n*n + a mod n")
 prefer 2
 apply(simp add: div_mult_mod_eq [symmetric])
apply(subgoal_tac "b - a ≤ b - c")
 prefer 2 apply arith
apply(drule le_less_trans)
back
 apply assumption
apply(frule less_not_refl2)
apply(drule less_imp_le)
apply (drule_tac m = "a" and k = n in div_le_mono)
apply(safe)
apply(frule_tac b = "b" and a = "a" and n = "n" in nat_lemma2, assumption, assumption)
apply assumption
apply(drule order_antisym, assumption)
apply(rotate_tac -3)
apply(simp)
done


subsubsection ‹Producer/Consumer Algorithm›

record Producer_consumer =
  ins :: nat
  outs :: nat
  li :: nat
  lj :: nat
  vx :: nat
  vy :: nat
  buffer :: "nat list"
  b :: "nat list"

text ‹The whole proof takes aprox. 4 minutes.›

lemma Producer_consumer:
  "[INIT= «0∧ 0🍋buffer ∧ length 🍋b=length a¬ ;
    I= «(∀k<🍋ins. 🍋outs≤k ⟶ (a ! k) = 🍋buffer ! (k mod (length 🍋buffer))) ∧
            🍋outs≤🍋ins ∧ 🍋ins-🍋outs≤length 🍋buffer¬ ;
    I1= «🍋I ∧ 🍋li≤length a¬ ;
    p1= «🍋I1 ∧ 🍋li=🍋ins¬ ;
    I2 = «🍋I ∧ (∀k<🍋lj. (a ! k)=(🍋b ! k)) ∧ 🍋lj≤length a¬ ;
    p2 = «🍋I2 ∧ 🍋lj=🍋outs¬ ] ==>
  ∥- {🍋INIT}
 🍋ins:=0,, 🍋outs:=0,, 🍋li:=0,, 🍋lj:=0,,
 COBEGIN {🍋p1 ∧ 🍋INIT}
   WHILE 🍋li
     INV {🍋p1 ∧ 🍋INIT}
   DO {🍋p1 ∧ 🍋INIT ∧ 🍋li}
       🍋vx:= (a ! 🍋li);;
      {🍋p1 ∧ 🍋INIT ∧ 🍋li∧ 🍋vx=(a ! 🍋li)}
        WAIT 🍋ins-🍋outs < length 🍋buffer END;;
      {🍋p1 ∧ 🍋INIT ∧ 🍋li∧ 🍋vx=(a ! 🍋li)
         ∧ 🍋ins-🍋outs < length 🍋buffer}
       🍋buffer:=(list_update 🍋buffer (🍋ins mod (length 🍋buffer)) 🍋vx);;
      {🍋p1 ∧ 🍋INIT ∧ 🍋li
         ∧ (a ! 🍋li)=(🍋buffer ! (🍋ins mod (length 🍋buffer)))
         ∧ 🍋ins-🍋outs 🍋buffer}
       🍋ins:=🍋ins+1;;
      {🍋I1 ∧ 🍋INIT ∧ (🍋li+1)=🍋ins ∧ 🍋li}
       🍋li:=🍋li+1
   OD
  {🍋p1 ∧ 🍋INIT ∧ 🍋li=length a}
  ∥
  {🍋p2 ∧ 🍋INIT}
   WHILE 🍋lj < length a
     INV {🍋p2 ∧ 🍋INIT}
   DO {🍋p2 ∧ 🍋lj∧ 🍋INIT}
        WAIT 🍋outs<🍋ins END;;
      {🍋p2 ∧ 🍋lj∧ 🍋outs<🍋ins ∧ 🍋INIT}
       🍋vy:=(🍋buffer ! (🍋outs mod (length 🍋buffer)));;
      {🍋p2 ∧ 🍋lj∧ 🍋outs<🍋ins ∧ 🍋vy=(a ! 🍋lj) ∧ 🍋INIT}
       🍋outs:=🍋outs+1;;
      {🍋I2 ∧ (🍋lj+1)=🍋outs ∧ 🍋lj∧ 🍋vy=(a ! 🍋lj) ∧ 🍋INIT}
       🍋b:=(list_update 🍋b 🍋lj 🍋vy);;
      {🍋I2 ∧ (🍋lj+1)=🍋outs ∧ 🍋lj∧ (a ! 🍋lj)=(🍋b ! 🍋lj) ∧ 🍋INIT}
       🍋lj:=🍋lj+1
   OD
  {🍋p2 ∧ 🍋lj=length a ∧ 🍋INIT}
 COEND
 { ∀k🍋b ! k)}"
apply oghoare
🍋 ‹138 vc›
apply(tactic ‹ALLGOALS (clarify_tac 🍋)›)
🍋 ‹112 subgoals left›
apply(simp_all (no_asm))
🍋 ‹43 subgoals left›
apply(tactic ‹ALLGOALS (conjI_Tac 🍋 (K all_tac))›)
🍋 ‹419 subgoals left›
apply(tactic ‹ALLGOALS (clarify_tac 🍋)›)
🍋 ‹99 subgoals left›
apply(simp_all only:length_0_conv [THEN sym])
🍋 ‹20 subgoals left›
apply (simp_all del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
🍋 ‹9 subgoals left›
apply (force simp add:less_Suc_eq)
apply(hypsubst_thin, drule sym)
apply (force simp add:less_Suc_eq)+
done

subsection ‹Parameterized Examples›

subsubsection ‹Set Elements of an Array to Zero›

record Example1 =
  a :: "nat ==> nat"

lemma Example1:
 "∥- {True}
   COBEGIN SCHEME [0≤i{True} 🍋a:=🍋a (i:=0) {🍋a i=0} COEND
  {∀i < n. 🍋a i = 0}"
apply oghoare
apply simp_all
done

text ‹Same example with lists as auxiliary variables.›
record Example1_list =
  A :: "nat list"
lemma Example1_list:
 "∥- {n < length 🍋A}
   COBEGIN
     SCHEME [0≤i{n < length 🍋A} 🍋A:=🍋A[i:=0] {🍋A!i=0}
   COEND
    {∀i < n. 🍋A!i = 0}"
apply oghoare
apply force+
done

subsubsection ‹Increment a Variable in Parallel›

text ‹First some lemmas about summation properties.›
(*
 lemma Example2_lemma1: "!!b. j🚫==> (∑i::nat🚫 b i) = (0::nat) ==> b j = 0 "
 apply(induct n)
  apply simp_all
 apply(force simp add: less_Suc_eq)
 done
*)
lemma Example2_lemma2_aux: "!!b. j==>
 (∑i=0..
 (∑i=0..∑i=0..
apply(induct n)
 apply simp_all
apply(simp add:less_Suc_eq)
 apply(auto)
apply(subgoal_tac "n - j = Suc(n- Suc j)")
  apply simp
apply arith
done

lemma Example2_lemma2_aux2:
  "!!b. j≤ s ==> (∑i::nat=0..∑i=0..
apply(induct j)
 apply simp_all
done

lemma Example2_lemma2:
 "!!b. [j] ==> Suc (∑i::nat=0..∑i=0..
apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
apply(erule_tac  t="sum (b(j := (Suc 0))) {0.. in ssubst)
apply(frule_tac b=b in Example2_lemma2_aux)
apply(erule_tac  t="sum b {0.. in ssubst)
apply(subgoal_tac "Suc (sum b {0..∑i=0..∑i=0..)
apply(rotate_tac -1)
apply(erule ssubst)
apply(subgoal_tac "j≤j")
 apply(drule_tac b="b" and t="(Suc 0)" in Example2_lemma2_aux2)
apply(rotate_tac -1)
apply(erule ssubst)
apply simp_all
done


record Example2 =
 c :: "nat ==> nat"
 x :: nat

lemma Example_2: "0==>
 ∥- {🍋x=0 ∧ (∑i=0..🍋c i)=0}
 COBEGIN
   SCHEME [0≤i
  {🍋x=(∑i=0..🍋c i) ∧ 🍋c i=0}
   ⟨ 🍋x:=🍋x+(Suc 0),, 🍋c:=🍋c (i:=(Suc 0)) ⟩
  {🍋x=(∑i=0..🍋c i) ∧ 🍋c i=(Suc 0)}
 COEND
 {🍋x=n}"
apply oghoare
apply (simp_all cong del: sum.cong_simp)
apply (tactic ‹ALLGOALS (clarify_tac 🍋)›)
apply (simp_all cong del: sum.cong_simp)
   apply(erule (1) Example2_lemma2)
  apply(erule (1) Example2_lemma2)
 apply(erule (1) Example2_lemma2)
apply(simp)
done

end