Pudding/Thread.v at master · jtcriswell/Pudding · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
(*
 * Module: Thread
 *
 * Description:
 *  This module defines an SVA Thread that is used in the small-step semantics.
 *
 * Note:
 *  Some of the code for the ThreadList comes from "Software Foundations" by
 *  Benjamin Pierce et. al.
 *)

(* Load Coq Standard Library modules *)
Require Import Arith.
Require Import Bool.
Require Import List.

(* Load SVA Library Modules *)
Require Export IC.

(*
 * Define an SVA thread which includes the following fields:
 *
 *  o A boolean flag indicating whether the state can be swapped on to the CPU
 *  o A program counter value
 *  o A stack of interrupt contexts for interrupts
 *  o A stack of interrupt contexts for saving interrupt contexts
 *)
Inductive SVAThread : Type :=
  | Thread : bool ->
             nat ->
             ICStack ->
             ICStack ->
             SVAThread.
Definition emptyThread := Thread false 0 nil nil.

(*
 * Define a set of SVAThreads.
 *)
Definition ThreadList := list SVAThread.
Definition emptyTL := nil : list SVAThread.
Definition getThread (id : nat) (t : ThreadList) := nth id t emptyThread.
Fixpoint updateThread (id:nat) (thread:SVAThread) (tl:ThreadList) : ThreadList :=
  match tl with
  | nil => nil
  | h :: t =>
    match id with
    | O => thread :: t
    | S n' => h :: updateThread n' thread t
    end
  end.

Definition getThreadPC (t : SVAThread) :=
  match t with
  | Thread valid PC stack istack => PC
end.

Definition canThreadSwap (t : SVAThread) :=
  match t with
  | Thread canSwap PC stack istack => canSwap
end.

Definition getThreadICL (t : SVAThread) :=
  match t with
  | Thread canSwap PC stack istack => stack
  end.

Definition getThreadSICL (t : SVAThread) :=
  match t with
  | Thread canSwap PC stack istack => istack
  end.

Definition getThreadICList (id : nat) (tl : ThreadList) :=
  getThreadICL (getThread id tl).

Definition getThreadSICList (id : nat) (tl : ThreadList) :=
  getThreadSICL (getThread id tl).

Definition threadOnCPU (newpc : nat) (t : SVAThread) :=
  match t with
  | Thread canSwap PC stack istack => Thread true newpc stack istack
end.

Definition threadOffCPU (t : SVAThread) :=
  match t with
  | Thread canSwap PC stack istack => Thread false 0 stack istack
end.

Definition pushSIC (tid : nat) (tl : ThreadList) :=
  updateThread  tid
                (Thread
                  false
                  (getThreadPC (getThread tid tl))
                  (getThreadICList tid tl)
                  (push
                    (itop (getThreadICList tid tl))
                    (getThreadSICList tid tl)))
                tl.

Definition popSIC (tid : nat) (tl : ThreadList) :=
  updateThread  tid
                (Thread
                  false
                  (getThreadPC (getThread tid tl))
                  (push
                    (itop (getThreadSICList tid tl))
                    (pop (getThreadICList tid tl)))
                  (pop (getThreadSICList tid tl)))
                tl.

Definition pushIC (Reg PC SP: nat) (tid : nat) (tl : ThreadList) :=
  updateThread  tid
                (Thread
                  false
                  (getThreadPC (getThread tid tl))
                  (push (IC Reg PC SP 0) (pop (getThreadICList tid tl)))
                  (getThreadSICList tid tl))
                tl.
(*
 * Theorem: updateMaintainListLength
 *
 * Description:
 *  Prove that updating an element in a thread list does not modify
 *  its length.
 *)
Theorem updateMaintainsListLength: forall (tid : nat) (t :SVAThread) (tl :ThreadList),
length tl = length (updateThread tid t tl).
Proof.
intros.
generalize dependent tid.
induction tl.

(* Case 1: Base case: empty list *)
intros.
simpl.
unfold updateThread.
destruct tid.
auto.
auto.

(* Case 2: Induction case: non-empty thread list *)
intros.
simpl.
destruct tid.

unfold updateThread.
simpl.
auto.

unfold updateThread.
simpl.
auto.
Qed.