author | wenzelm |
Fri, 02 Sep 2005 17:23:59 +0200 | |
changeset 17233 | 41eee2e7b465 |
parent 14981 | e73f8140af78 |
child 17955 | 3b34516662c6 |
permissions | -rw-r--r-- |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
1 |
(* Title: HOLCF/IOA/meta_theory/Deadlock.ML |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
2 |
ID: $Id$ |
12218 | 3 |
Author: Olaf Müller |
17233 | 4 |
*) |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
5 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
6 |
(******************************************************************************** |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
7 |
input actions may always be added to a schedule |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
8 |
**********************************************************************************) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
9 |
|
10835 | 10 |
Goal "[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|] \ |
11 |
\ ==> Filter (%x. x:act A)$sch @@ a>>nil : schedules A"; |
|
4098 | 12 |
by (asm_full_simp_tac (simpset() addsimps [schedules_def,has_schedule_def]) 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
13 |
by (safe_tac set_cs); |
7499 | 14 |
by (ftac inp_is_act 1); |
4098 | 15 |
by (asm_full_simp_tac (simpset() addsimps [executions_def]) 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
16 |
by (pair_tac "ex" 1); |
6161 | 17 |
ren "s ex" 1; |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
18 |
by (subgoal_tac "Finite ex" 1); |
4098 | 19 |
by (asm_full_simp_tac (simpset() addsimps [filter_act_def]) 2); |
3457 | 20 |
by (rtac (Map2Finite RS iffD1) 2); |
10835 | 21 |
by (res_inst_tac [("t","Map fst$ex")] subst 2); |
3457 | 22 |
by (assume_tac 2); |
23 |
by (etac FiniteFilter 2); |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
24 |
(* subgoal 1 *) |
7499 | 25 |
by (ftac exists_laststate 1); |
3457 | 26 |
by (etac allE 1); |
27 |
by (etac exE 1); |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
28 |
(* using input-enabledness *) |
4098 | 29 |
by (asm_full_simp_tac (simpset() addsimps [input_enabled_def]) 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
30 |
by (REPEAT (etac conjE 1)); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
31 |
by (eres_inst_tac [("x","a")] allE 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
32 |
by (Asm_full_simp_tac 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
33 |
by (eres_inst_tac [("x","u")] allE 1); |
3457 | 34 |
by (etac exE 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
35 |
(* instantiate execution *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
36 |
by (res_inst_tac [("x","(s,ex @@ (a,s2)>>nil)")] exI 1); |
4098 | 37 |
by (asm_full_simp_tac (simpset() addsimps [filter_act_def,MapConc]) 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
38 |
by (eres_inst_tac [("t","u")] lemma_2_1 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
39 |
by (Asm_full_simp_tac 1); |
3457 | 40 |
by (rtac sym 1); |
41 |
by (assume_tac 1); |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
42 |
qed"scheds_input_enabled"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
43 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
44 |
(******************************************************************************** |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
45 |
Deadlock freedom: component B cannot block an out or int action |
3521 | 46 |
of component A in every schedule. |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
47 |
Needs compositionality on schedule level, input-enabledness, compatibility |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
48 |
and distributivity of is_exec_frag over @@ |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
49 |
**********************************************************************************) |
4833 | 50 |
Delsplits [split_if]; |
6161 | 51 |
Goal "[| a : local A; Finite sch; sch : schedules (A||B); \ |
10835 | 52 |
\ Filter (%x. x:act A)$(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |] \ |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
53 |
\ ==> (sch @@ a>>nil) : schedules (A||B)"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
54 |
|
4098 | 55 |
by (asm_full_simp_tac (simpset() addsimps [compositionality_sch,locals_def]) 1); |
3457 | 56 |
by (rtac conjI 1); |
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
57 |
(* a : act (A||B) *) |
4098 | 58 |
by (asm_full_simp_tac (simpset() addsimps [actions_of_par]) 2); |
5132 | 59 |
by (blast_tac (claset() addDs [int_is_act,out_is_act]) 2); |
4681 | 60 |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
61 |
(* Filter B (sch@@[a]) : schedules B *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
62 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
63 |
by (case_tac "a:int A" 1); |
3457 | 64 |
by (dtac intA_is_not_actB 1); |
65 |
by (assume_tac 1); (* --> a~:act B *) |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
66 |
by (Asm_full_simp_tac 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
67 |
|
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
68 |
(* case a~:int A , i.e. a:out A *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
69 |
by (case_tac "a~:act B" 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
70 |
by (Asm_full_simp_tac 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
71 |
(* case a:act B *) |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
72 |
by (Asm_full_simp_tac 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
73 |
by (subgoal_tac "a:out A" 1); |
4681 | 74 |
by (Blast_tac 2); |
3457 | 75 |
by (dtac outAactB_is_inpB 1); |
76 |
by (assume_tac 1); |
|
77 |
by (assume_tac 1); |
|
78 |
by (rtac scheds_input_enabled 1); |
|
3433
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
79 |
by (Asm_full_simp_tac 1); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
80 |
by (REPEAT (atac 1)); |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
81 |
qed"IOA_deadlock_free"; |
2de17c994071
added deadlock freedom, polished definitions and proofs
mueller
parents:
diff
changeset
|
82 |
|
4833 | 83 |
Addsplits [split_if]; |