src/HOL/UNITY/Mutex.ML
author paulson
Fri Apr 03 12:34:33 1998 +0200 (1998-04-03)
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
permissions -rw-r--r--
New UNITY theory
     1 (*  Title:      HOL/UNITY/Mutex.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
     7 *)
     8 
     9 open Mutex;
    10 
    11 val cmd_defs = [mutex_def, cmd0_def, cmd1u_def, cmd1v_def, 
    12 		cmd2_def, cmd3_def, cmd4_def];
    13 
    14 goalw thy [mutex_def] "id : mutex";
    15 by (Simp_tac 1);
    16 qed "id_in_mutex";
    17 AddIffs [id_in_mutex];
    18 
    19 
    20 (** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
    21 
    22 (*proves "constrains" properties when the program is specified*)
    23 val constrains_tac = 
    24    SELECT_GOAL
    25       (EVERY [rtac constrainsI 1,
    26 	      rewtac mutex_def,
    27 	      REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
    28 	      rewrite_goals_tac cmd_defs,
    29 	      ALLGOALS (SELECT_GOAL Auto_tac)]);
    30 
    31 
    32 (*proves "ensures" properties when the program is specified*)
    33 fun ensures_tac sact = 
    34     SELECT_GOAL
    35       (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
    36 	      res_inst_tac [("act", sact)] transient_mem 2,
    37 	      Simp_tac 2,
    38 	      constrains_tac 1,
    39 	      rewrite_goals_tac cmd_defs,
    40 	      Auto_tac]);
    41 
    42 
    43 (*The booleans p, u, v are always either 0 or 1*)
    44 goalw thy [stable_def, boolVars_def]
    45     "stable mutex boolVars";
    46 by (constrains_tac 1);
    47 by (auto_tac (claset() addSEs [less_SucE], simpset()));
    48 qed "stable_boolVars";
    49 
    50 goal thy "reachable MInit mutex <= boolVars";
    51 by (rtac strongest_invariant 1);
    52 by (rtac stable_boolVars 2);
    53 by (rewrite_goals_tac [MInit_def, boolVars_def]);
    54 by Auto_tac;
    55 qed "reachable_subset_boolVars";
    56 
    57 val reachable_subset_boolVars' = 
    58     rewrite_rule [boolVars_def] reachable_subset_boolVars;
    59 
    60 goalw thy [stable_def, invariant_def]
    61     "stable mutex (invariant 0 UU MM)";
    62 by (constrains_tac 1);
    63 qed "stable_invar_0um";
    64 
    65 goalw thy [stable_def, invariant_def]
    66     "stable mutex (invariant 1 VV NN)";
    67 by (constrains_tac 1);
    68 qed "stable_invar_1vn";
    69 
    70 goalw thy [MInit_def, invariant_def] "MInit <= invariant 0 UU MM";
    71 by Auto_tac;
    72 qed "MInit_invar_0um";
    73 
    74 goalw thy [MInit_def, invariant_def] "MInit <= invariant 1 VV NN";
    75 by Auto_tac;
    76 qed "MInit_invar_1vn";
    77 
    78 (*The intersection is an invariant of the system*)
    79 goal thy "reachable MInit mutex <= invariant 0 UU MM Int invariant 1 VV NN";
    80 by (simp_tac (simpset() addsimps
    81 	      [strongest_invariant, Int_greatest, stable_Int, 
    82 	       stable_invar_0um, stable_invar_1vn, 
    83 	       MInit_invar_0um,MInit_invar_1vn]) 1); 
    84 qed "reachable_subset_invariant";
    85 
    86 val reachable_subset_invariant' = 
    87     rewrite_rule [invariant_def] reachable_subset_invariant;
    88 
    89 
    90 (*The safety property (mutual exclusion) follows from the claimed invar_s*)
    91 goalw thy [invariant_def]
    92     "{s. s MM = 3 & s NN = 3} <= \
    93 \    Compl (invariant 0 UU MM Int invariant 1 VV NN)";
    94 by Auto_tac;
    95 val lemma = result();
    96 
    97 goal thy "{s. s MM = 3 & s NN = 3} <= Compl (reachable MInit mutex)";
    98 by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono] MRS subset_trans) 1);
    99 qed "mutual_exclusion";
   100 
   101 
   102 (*The bad invariant FAILS in cmd1v*)
   103 goalw thy [stable_def, bad_invariant_def]
   104     "stable mutex (bad_invariant 0 UU MM)";
   105 by (constrains_tac 1);
   106 by (trans_tac 1);
   107 by (safe_tac (claset() addSEs [le_SucE]));
   108 by (Asm_full_simp_tac 1);
   109 (*Resulting state: n=1, p=false, m=4, u=false.  
   110   Execution of cmd1v (the command of process v guarded by n=1) sets p:=true,
   111   violating the invariant!*)
   112 (*Check that subgoals remain: proof failed.*)
   113 getgoal 1;  
   114 
   115 
   116 (*** Progress for U ***)
   117 
   118 goalw thy [unless_def] "unless mutex {s. s MM=2} {s. s MM=3}";
   119 by (constrains_tac 1);
   120 qed "U_F0";
   121 
   122 goal thy "LeadsTo MInit mutex {s. s MM=1} {s. s PP = s VV & s MM = 2}";
   123 by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
   124 by (ensures_tac "cmd1u" 1);
   125 qed "U_F1";
   126 
   127 goal thy "LeadsTo MInit mutex {s. s PP = 0 & s MM = 2} {s. s MM = 3}";
   128 by (cut_facts_tac [reachable_subset_invariant'] 1);
   129 by (ensures_tac "cmd2 0 MM" 1);
   130 qed "U_F2";
   131 
   132 goalw thy [mutex_def] "LeadsTo MInit mutex {s. s MM = 3} {s. s PP = 1}";
   133 by (rtac leadsTo_imp_LeadsTo 1); 
   134 by (res_inst_tac [("B", "{s. s MM = 4}")] leadsTo_Trans 1);
   135 by (ensures_tac "cmd4 1 MM" 2);
   136 by (ensures_tac "cmd3 UU MM" 1);
   137 qed "U_F3";
   138 
   139 goal thy "LeadsTo MInit mutex {s. s MM = 2} {s. s PP = 1}";
   140 by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
   141 	  MRS LeadsTo_Diff) 1);
   142 by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
   143 by (cut_facts_tac [reachable_subset_boolVars'] 1);
   144 by (auto_tac (claset() addSEs [less_SucE], simpset()));
   145 val lemma2 = result();
   146 
   147 goal thy "LeadsTo MInit mutex {s. s MM = 1} {s. s PP = 1}";
   148 by (rtac ([U_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
   149 by (Blast_tac 1);
   150 val lemma1 = result();
   151 
   152 
   153 goal thy "LeadsTo MInit mutex {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}";
   154 by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
   155 	                addcongs [rev_conj_cong]) 1);
   156 by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
   157 				  lemma1, lemma2, U_F3] ) 1);
   158 val lemma123 = result();
   159 
   160 
   161 (*Misra's F4*)
   162 goal thy "LeadsTo MInit mutex {s. s UU = 1} {s. s PP = 1}";
   163 by (rtac LeadsTo_weaken_L 1);
   164 by (rtac lemma123 1);
   165 by (cut_facts_tac [reachable_subset_invariant'] 1);
   166 by Auto_tac;
   167 qed "u_leadsto_p";
   168 
   169 
   170 (*** Progress for V ***)
   171 
   172 
   173 goalw thy [unless_def] "unless mutex {s. s NN=2} {s. s NN=3}";
   174 by (constrains_tac 1);
   175 qed "V_F0";
   176 
   177 goal thy "LeadsTo MInit mutex {s. s NN=1} {s. s PP = 1 - s UU & s NN = 2}";
   178 by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
   179 by (ensures_tac "cmd1v" 1);
   180 qed "V_F1";
   181 
   182 goal thy "LeadsTo MInit mutex {s. s PP = 1 & s NN = 2} {s. s NN = 3}";
   183 by (cut_facts_tac [reachable_subset_invariant'] 1);
   184 by (ensures_tac "cmd2 1 NN" 1);
   185 qed "V_F2";
   186 
   187 goalw thy [mutex_def] "LeadsTo MInit mutex {s. s NN = 3} {s. s PP = 0}";
   188 by (rtac leadsTo_imp_LeadsTo 1); 
   189 by (res_inst_tac [("B", "{s. s NN = 4}")] leadsTo_Trans 1);
   190 by (ensures_tac "cmd4 0 NN" 2);
   191 by (ensures_tac "cmd3 VV NN" 1);
   192 qed "V_F3";
   193 
   194 goal thy "LeadsTo MInit mutex {s. s NN = 2} {s. s PP = 0}";
   195 by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
   196 	  MRS LeadsTo_Diff) 1);
   197 by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
   198 by (cut_facts_tac [reachable_subset_boolVars'] 1);
   199 by (auto_tac (claset() addSEs [less_SucE], simpset()));
   200 val lemma2 = result();
   201 
   202 goal thy "LeadsTo MInit mutex {s. s NN = 1} {s. s PP = 0}";
   203 by (rtac ([V_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
   204 by (Blast_tac 1);
   205 val lemma1 = result();
   206 
   207 
   208 goal thy "LeadsTo MInit mutex {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}";
   209 by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
   210 	                addcongs [rev_conj_cong]) 1);
   211 by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
   212 				  lemma1, lemma2, V_F3] ) 1);
   213 val lemma123 = result();
   214 
   215 
   216 (*Misra's F4*)
   217 goal thy "LeadsTo MInit mutex {s. s VV = 1} {s. s PP = 0}";
   218 by (rtac LeadsTo_weaken_L 1);
   219 by (rtac lemma123 1);
   220 by (cut_facts_tac [reachable_subset_invariant'] 1);
   221 by Auto_tac;
   222 qed "v_leadsto_not_p";
   223 
   224 
   225 (** Absence of starvation **)
   226 
   227 (*Misra's F6*)
   228 goal thy "LeadsTo MInit mutex {s. s MM = 1} {s. s MM = 3}";
   229 by (rtac LeadsTo_Un_duplicate 1);
   230 by (rtac LeadsTo_cancel2 1);
   231 by (rtac U_F2 2);
   232 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
   233 by (stac Un_commute 1);
   234 by (rtac LeadsTo_Un_duplicate 1);
   235 by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
   236 by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
   237 by (cut_facts_tac [reachable_subset_boolVars'] 1);
   238 by (auto_tac (claset() addSEs [less_SucE], simpset()));
   239 qed "m1_leadsto_3";
   240 
   241 
   242 (*The same for V*)
   243 goal thy "LeadsTo MInit mutex {s. s NN = 1} {s. s NN = 3}";
   244 by (rtac LeadsTo_Un_duplicate 1);
   245 by (rtac LeadsTo_cancel2 1);
   246 by (rtac V_F2 2);
   247 by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
   248 by (stac Un_commute 1);
   249 by (rtac LeadsTo_Un_duplicate 1);
   250 by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
   251 by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
   252 by (cut_facts_tac [reachable_subset_boolVars'] 1);
   253 by (auto_tac (claset() addSEs [less_SucE], simpset()));
   254 qed "n1_leadsto_3";