src/HOL/UNITY/Mutex.ML
changeset 4776 1f9362e769c1
child 5069 3ea049f7979d
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Mutex.ML	Fri Apr 03 12:34:33 1998 +0200
     1.3 @@ -0,0 +1,254 @@
     1.4 +(*  Title:      HOL/UNITY/Mutex.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +Based on "A Family of 2-Process Mutual Exclusion Algorithms" by J Misra
    1.10 +*)
    1.11 +
    1.12 +open Mutex;
    1.13 +
    1.14 +val cmd_defs = [mutex_def, cmd0_def, cmd1u_def, cmd1v_def, 
    1.15 +		cmd2_def, cmd3_def, cmd4_def];
    1.16 +
    1.17 +goalw thy [mutex_def] "id : mutex";
    1.18 +by (Simp_tac 1);
    1.19 +qed "id_in_mutex";
    1.20 +AddIffs [id_in_mutex];
    1.21 +
    1.22 +
    1.23 +(** Constrains/Ensures tactics: NEED TO BE GENERALIZED OVER ALL PROGRAMS **)
    1.24 +
    1.25 +(*proves "constrains" properties when the program is specified*)
    1.26 +val constrains_tac = 
    1.27 +   SELECT_GOAL
    1.28 +      (EVERY [rtac constrainsI 1,
    1.29 +	      rewtac mutex_def,
    1.30 +	      REPEAT_FIRST (eresolve_tac [insertE, emptyE]),
    1.31 +	      rewrite_goals_tac cmd_defs,
    1.32 +	      ALLGOALS (SELECT_GOAL Auto_tac)]);
    1.33 +
    1.34 +
    1.35 +(*proves "ensures" properties when the program is specified*)
    1.36 +fun ensures_tac sact = 
    1.37 +    SELECT_GOAL
    1.38 +      (EVERY [REPEAT (resolve_tac [LeadsTo_Basis, leadsTo_Basis, ensuresI] 1),
    1.39 +	      res_inst_tac [("act", sact)] transient_mem 2,
    1.40 +	      Simp_tac 2,
    1.41 +	      constrains_tac 1,
    1.42 +	      rewrite_goals_tac cmd_defs,
    1.43 +	      Auto_tac]);
    1.44 +
    1.45 +
    1.46 +(*The booleans p, u, v are always either 0 or 1*)
    1.47 +goalw thy [stable_def, boolVars_def]
    1.48 +    "stable mutex boolVars";
    1.49 +by (constrains_tac 1);
    1.50 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
    1.51 +qed "stable_boolVars";
    1.52 +
    1.53 +goal thy "reachable MInit mutex <= boolVars";
    1.54 +by (rtac strongest_invariant 1);
    1.55 +by (rtac stable_boolVars 2);
    1.56 +by (rewrite_goals_tac [MInit_def, boolVars_def]);
    1.57 +by Auto_tac;
    1.58 +qed "reachable_subset_boolVars";
    1.59 +
    1.60 +val reachable_subset_boolVars' = 
    1.61 +    rewrite_rule [boolVars_def] reachable_subset_boolVars;
    1.62 +
    1.63 +goalw thy [stable_def, invariant_def]
    1.64 +    "stable mutex (invariant 0 UU MM)";
    1.65 +by (constrains_tac 1);
    1.66 +qed "stable_invar_0um";
    1.67 +
    1.68 +goalw thy [stable_def, invariant_def]
    1.69 +    "stable mutex (invariant 1 VV NN)";
    1.70 +by (constrains_tac 1);
    1.71 +qed "stable_invar_1vn";
    1.72 +
    1.73 +goalw thy [MInit_def, invariant_def] "MInit <= invariant 0 UU MM";
    1.74 +by Auto_tac;
    1.75 +qed "MInit_invar_0um";
    1.76 +
    1.77 +goalw thy [MInit_def, invariant_def] "MInit <= invariant 1 VV NN";
    1.78 +by Auto_tac;
    1.79 +qed "MInit_invar_1vn";
    1.80 +
    1.81 +(*The intersection is an invariant of the system*)
    1.82 +goal thy "reachable MInit mutex <= invariant 0 UU MM Int invariant 1 VV NN";
    1.83 +by (simp_tac (simpset() addsimps
    1.84 +	      [strongest_invariant, Int_greatest, stable_Int, 
    1.85 +	       stable_invar_0um, stable_invar_1vn, 
    1.86 +	       MInit_invar_0um,MInit_invar_1vn]) 1); 
    1.87 +qed "reachable_subset_invariant";
    1.88 +
    1.89 +val reachable_subset_invariant' = 
    1.90 +    rewrite_rule [invariant_def] reachable_subset_invariant;
    1.91 +
    1.92 +
    1.93 +(*The safety property (mutual exclusion) follows from the claimed invar_s*)
    1.94 +goalw thy [invariant_def]
    1.95 +    "{s. s MM = 3 & s NN = 3} <= \
    1.96 +\    Compl (invariant 0 UU MM Int invariant 1 VV NN)";
    1.97 +by Auto_tac;
    1.98 +val lemma = result();
    1.99 +
   1.100 +goal thy "{s. s MM = 3 & s NN = 3} <= Compl (reachable MInit mutex)";
   1.101 +by (rtac ([lemma, reachable_subset_invariant RS Compl_anti_mono] MRS subset_trans) 1);
   1.102 +qed "mutual_exclusion";
   1.103 +
   1.104 +
   1.105 +(*The bad invariant FAILS in cmd1v*)
   1.106 +goalw thy [stable_def, bad_invariant_def]
   1.107 +    "stable mutex (bad_invariant 0 UU MM)";
   1.108 +by (constrains_tac 1);
   1.109 +by (trans_tac 1);
   1.110 +by (safe_tac (claset() addSEs [le_SucE]));
   1.111 +by (Asm_full_simp_tac 1);
   1.112 +(*Resulting state: n=1, p=false, m=4, u=false.  
   1.113 +  Execution of cmd1v (the command of process v guarded by n=1) sets p:=true,
   1.114 +  violating the invariant!*)
   1.115 +(*Check that subgoals remain: proof failed.*)
   1.116 +getgoal 1;  
   1.117 +
   1.118 +
   1.119 +(*** Progress for U ***)
   1.120 +
   1.121 +goalw thy [unless_def] "unless mutex {s. s MM=2} {s. s MM=3}";
   1.122 +by (constrains_tac 1);
   1.123 +qed "U_F0";
   1.124 +
   1.125 +goal thy "LeadsTo MInit mutex {s. s MM=1} {s. s PP = s VV & s MM = 2}";
   1.126 +by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
   1.127 +by (ensures_tac "cmd1u" 1);
   1.128 +qed "U_F1";
   1.129 +
   1.130 +goal thy "LeadsTo MInit mutex {s. s PP = 0 & s MM = 2} {s. s MM = 3}";
   1.131 +by (cut_facts_tac [reachable_subset_invariant'] 1);
   1.132 +by (ensures_tac "cmd2 0 MM" 1);
   1.133 +qed "U_F2";
   1.134 +
   1.135 +goalw thy [mutex_def] "LeadsTo MInit mutex {s. s MM = 3} {s. s PP = 1}";
   1.136 +by (rtac leadsTo_imp_LeadsTo 1); 
   1.137 +by (res_inst_tac [("B", "{s. s MM = 4}")] leadsTo_Trans 1);
   1.138 +by (ensures_tac "cmd4 1 MM" 2);
   1.139 +by (ensures_tac "cmd3 UU MM" 1);
   1.140 +qed "U_F3";
   1.141 +
   1.142 +goal thy "LeadsTo MInit mutex {s. s MM = 2} {s. s PP = 1}";
   1.143 +by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
   1.144 +	  MRS LeadsTo_Diff) 1);
   1.145 +by (rtac ([U_F2, U_F3] MRS LeadsTo_Trans) 1);
   1.146 +by (cut_facts_tac [reachable_subset_boolVars'] 1);
   1.147 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
   1.148 +val lemma2 = result();
   1.149 +
   1.150 +goal thy "LeadsTo MInit mutex {s. s MM = 1} {s. s PP = 1}";
   1.151 +by (rtac ([U_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
   1.152 +by (Blast_tac 1);
   1.153 +val lemma1 = result();
   1.154 +
   1.155 +
   1.156 +goal thy "LeadsTo MInit mutex {s. 1 <= s MM & s MM <= 3} {s. s PP = 1}";
   1.157 +by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
   1.158 +	                addcongs [rev_conj_cong]) 1);
   1.159 +by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
   1.160 +				  lemma1, lemma2, U_F3] ) 1);
   1.161 +val lemma123 = result();
   1.162 +
   1.163 +
   1.164 +(*Misra's F4*)
   1.165 +goal thy "LeadsTo MInit mutex {s. s UU = 1} {s. s PP = 1}";
   1.166 +by (rtac LeadsTo_weaken_L 1);
   1.167 +by (rtac lemma123 1);
   1.168 +by (cut_facts_tac [reachable_subset_invariant'] 1);
   1.169 +by Auto_tac;
   1.170 +qed "u_leadsto_p";
   1.171 +
   1.172 +
   1.173 +(*** Progress for V ***)
   1.174 +
   1.175 +
   1.176 +goalw thy [unless_def] "unless mutex {s. s NN=2} {s. s NN=3}";
   1.177 +by (constrains_tac 1);
   1.178 +qed "V_F0";
   1.179 +
   1.180 +goal thy "LeadsTo MInit mutex {s. s NN=1} {s. s PP = 1 - s UU & s NN = 2}";
   1.181 +by (rtac leadsTo_imp_LeadsTo 1);   (*makes the proof much faster*)
   1.182 +by (ensures_tac "cmd1v" 1);
   1.183 +qed "V_F1";
   1.184 +
   1.185 +goal thy "LeadsTo MInit mutex {s. s PP = 1 & s NN = 2} {s. s NN = 3}";
   1.186 +by (cut_facts_tac [reachable_subset_invariant'] 1);
   1.187 +by (ensures_tac "cmd2 1 NN" 1);
   1.188 +qed "V_F2";
   1.189 +
   1.190 +goalw thy [mutex_def] "LeadsTo MInit mutex {s. s NN = 3} {s. s PP = 0}";
   1.191 +by (rtac leadsTo_imp_LeadsTo 1); 
   1.192 +by (res_inst_tac [("B", "{s. s NN = 4}")] leadsTo_Trans 1);
   1.193 +by (ensures_tac "cmd4 0 NN" 2);
   1.194 +by (ensures_tac "cmd3 VV NN" 1);
   1.195 +qed "V_F3";
   1.196 +
   1.197 +goal thy "LeadsTo MInit mutex {s. s NN = 2} {s. s PP = 0}";
   1.198 +by (rtac ([LeadsTo_weaken_L, subset_refl RS subset_imp_LeadsTo] 
   1.199 +	  MRS LeadsTo_Diff) 1);
   1.200 +by (rtac ([V_F2, V_F3] MRS LeadsTo_Trans) 1);
   1.201 +by (cut_facts_tac [reachable_subset_boolVars'] 1);
   1.202 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
   1.203 +val lemma2 = result();
   1.204 +
   1.205 +goal thy "LeadsTo MInit mutex {s. s NN = 1} {s. s PP = 0}";
   1.206 +by (rtac ([V_F1 RS LeadsTo_weaken_R, lemma2] MRS LeadsTo_Trans) 1);
   1.207 +by (Blast_tac 1);
   1.208 +val lemma1 = result();
   1.209 +
   1.210 +
   1.211 +goal thy "LeadsTo MInit mutex {s. 1 <= s NN & s NN <= 3} {s. s PP = 0}";
   1.212 +by (simp_tac (simpset() addsimps [le_Suc_eq, conj_disj_distribL] 
   1.213 +	                addcongs [rev_conj_cong]) 1);
   1.214 +by (simp_tac (simpset() addsimps [Collect_disj_eq, LeadsTo_Un_distrib,
   1.215 +				  lemma1, lemma2, V_F3] ) 1);
   1.216 +val lemma123 = result();
   1.217 +
   1.218 +
   1.219 +(*Misra's F4*)
   1.220 +goal thy "LeadsTo MInit mutex {s. s VV = 1} {s. s PP = 0}";
   1.221 +by (rtac LeadsTo_weaken_L 1);
   1.222 +by (rtac lemma123 1);
   1.223 +by (cut_facts_tac [reachable_subset_invariant'] 1);
   1.224 +by Auto_tac;
   1.225 +qed "v_leadsto_not_p";
   1.226 +
   1.227 +
   1.228 +(** Absence of starvation **)
   1.229 +
   1.230 +(*Misra's F6*)
   1.231 +goal thy "LeadsTo MInit mutex {s. s MM = 1} {s. s MM = 3}";
   1.232 +by (rtac LeadsTo_Un_duplicate 1);
   1.233 +by (rtac LeadsTo_cancel2 1);
   1.234 +by (rtac U_F2 2);
   1.235 +by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
   1.236 +by (stac Un_commute 1);
   1.237 +by (rtac LeadsTo_Un_duplicate 1);
   1.238 +by (rtac ([v_leadsto_not_p, U_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
   1.239 +by (rtac (U_F1 RS LeadsTo_weaken_R) 1);
   1.240 +by (cut_facts_tac [reachable_subset_boolVars'] 1);
   1.241 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
   1.242 +qed "m1_leadsto_3";
   1.243 +
   1.244 +
   1.245 +(*The same for V*)
   1.246 +goal thy "LeadsTo MInit mutex {s. s NN = 1} {s. s NN = 3}";
   1.247 +by (rtac LeadsTo_Un_duplicate 1);
   1.248 +by (rtac LeadsTo_cancel2 1);
   1.249 +by (rtac V_F2 2);
   1.250 +by (simp_tac (simpset() addsimps [Collect_conj_eq] ) 1);
   1.251 +by (stac Un_commute 1);
   1.252 +by (rtac LeadsTo_Un_duplicate 1);
   1.253 +by (rtac ([u_leadsto_p, V_F0] MRS R_PSP_unless  RSN(2, LeadsTo_cancel2)) 1);
   1.254 +by (rtac (V_F1 RS LeadsTo_weaken_R) 1);
   1.255 +by (cut_facts_tac [reachable_subset_boolVars'] 1);
   1.256 +by (auto_tac (claset() addSEs [less_SucE], simpset()));
   1.257 +qed "n1_leadsto_3";