Theory OG_Examples

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<n ⟹ ∥- ⦃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; I=«n=length ´turn ∧ 0<´nextv ∧ (∀k l. k<n ∧ l<n ∧ 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 \<^context>)›)
― ‹11 vc›
apply simp_all
apply(tactic ‹ALLGOALS (clarify_tac \<^context>)›)
― ‹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<length a ∧ 0<length ´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 <length a
     INV ⦃´p1 ∧ ´INIT⦄
   DO ⦃´p1 ∧ ´INIT ∧ ´li<length a⦄
       ´vx:= (a ! ´li);;
      ⦃´p1 ∧ ´INIT ∧ ´li<length a ∧ ´vx=(a ! ´li)⦄
        WAIT ´ins-´outs < length ´buffer END;;
      ⦃´p1 ∧ ´INIT ∧ ´li<length a ∧ ´vx=(a ! ´li)
         ∧ ´ins-´outs < length ´buffer⦄
       ´buffer:=(list_update ´buffer (´ins mod (length ´buffer)) ´vx);;
      ⦃´p1 ∧ ´INIT ∧ ´li<length a
         ∧ (a ! ´li)=(´buffer ! (´ins mod (length ´buffer)))
         ∧ ´ins-´outs <length ´buffer⦄
       ´ins:=´ins+1;;
      ⦃´I1 ∧ ´INIT ∧ (´li+1)=´ins ∧ ´li<length a⦄
       ´li:=´li+1
   OD
  ⦃´p1 ∧ ´INIT ∧ ´li=length a⦄
  ∥
  ⦃´p2 ∧ ´INIT⦄
   WHILE ´lj < length a
     INV ⦃´p2 ∧ ´INIT⦄
   DO ⦃´p2 ∧ ´lj<length a ∧ ´INIT⦄
        WAIT ´outs<´ins END;;
      ⦃´p2 ∧ ´lj<length a ∧ ´outs<´ins ∧ ´INIT⦄
       ´vy:=(´buffer ! (´outs mod (length ´buffer)));;
      ⦃´p2 ∧ ´lj<length a ∧ ´outs<´ins ∧ ´vy=(a ! ´lj) ∧ ´INIT⦄
       ´outs:=´outs+1;;
      ⦃´I2 ∧ (´lj+1)=´outs ∧ ´lj<length a ∧ ´vy=(a ! ´lj) ∧ ´INIT⦄
       ´b:=(list_update ´b ´lj ´vy);;
      ⦃´I2 ∧ (´lj+1)=´outs ∧ ´lj<length a ∧ (a ! ´lj)=(´b ! ´lj) ∧ ´INIT⦄
       ´lj:=´lj+1
   OD
  ⦃´p2 ∧ ´lj=length a ∧ ´INIT⦄
 COEND
 ⦃ ∀k<length a. (a ! k)=(´b ! k)⦄"
apply oghoare
― ‹138 vc›
apply(tactic ‹ALLGOALS (clarify_tac \<^context>)›)
― ‹112 subgoals left›
apply(simp_all (no_asm))
― ‹43 subgoals left›
apply(tactic ‹ALLGOALS (conjI_Tac \<^context> (K all_tac))›)
― ‹419 subgoals left›
apply(tactic ‹ALLGOALS (clarify_tac \<^context>)›)
― ‹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<n] ⦃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] ⦃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<n ⟹ (∑i::nat<n. 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<n ⟹
 (∑i=0..<n. (b i::nat)) =
 (∑i=0..<j. b i) + b j + (∑i=0..<n-(Suc j) . b (Suc j + i))"
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..<j. (b (s:=t)) i) = (∑i=0..<j. b i)"
apply(induct j)
 apply simp_all
done

lemma Example2_lemma2:
 "!!b. ⟦j<n; b j=0⟧ ⟹ Suc (∑i::nat=0..<n. b i)=(∑i=0..<n. (b (j := Suc 0)) i)"
apply(frule_tac b="(b (j:=(Suc 0)))" in Example2_lemma2_aux)
apply(erule_tac  t="sum (b(j := (Suc 0))) {0..<n}" in ssubst)
apply(frule_tac b=b in Example2_lemma2_aux)
apply(erule_tac  t="sum b {0..<n}" in ssubst)
apply(subgoal_tac "Suc (sum b {0..<j} + b j + (∑i=0..<n - Suc j. b (Suc j + i)))=(sum b {0..<j} + Suc (b j) + (∑i=0..<n - Suc j. b (Suc j + i)))")
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<n ⟹
 ∥- ⦃´x=0 ∧ (∑i=0..<n. ´c i)=0⦄
 COBEGIN
   SCHEME [0≤i<n]
  ⦃´x=(∑i=0..<n. ´c i) ∧ ´c i=0⦄
   ⟨ ´x:=´x+(Suc 0),, ´c:=´c (i:=(Suc 0)) ⟩
  ⦃´x=(∑i=0..<n. ´c i) ∧ ´c i=(Suc 0)⦄
 COEND
 ⦃´x=n⦄"
apply oghoare
apply (simp_all cong del: sum.cong_simp)
apply (tactic ‹ALLGOALS (clarify_tac \<^context>)›)
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