Robert Allan James
422ef2fa29
Isabelle toolchain replaced (was genuinely 2011, 14+ years stale) and every theory file fixed to actually compile -- most had apparently never been checked under a working Isabelle at all. Fixed the vm_state self-reference in StarForth_Base.thy properly (word_table is now a free-standing global constant, not a circular record field), corrected the word_physics_transparent axiom (was claiming full state equality from mere exec-equivalence, provably too strong), and worked through 14 years of HOL-Library drift plus several missing-hypothesis bugs across the physics-loop and ACL theories. Two genuine (non-tactical) bugs found and left oops-flagged rather than silently resolved: forth_roll's index arithmetic disagrees with both its own test lemma and the real C ROLL implementation (three-way inconsistency), and pm_wf isn't actually preserved by pm_record_hit/pm_record_miss. Both need a decision, not a proof-script fix. Full writeup in FABRIC-2.md item 5.2.
194 lines
7.7 KiB
Plaintext
194 lines
7.7 KiB
Plaintext
theory StarForth_Mutex
|
|
imports StarForth_Base
|
|
begin
|
|
|
|
(* =========================================================================
|
|
StarForth_Mutex — Mutex / lock-state model
|
|
|
|
Mirrors: sf_mutex_t logic protecting tuning_lock and dict_lock in the VM.
|
|
|
|
The VM has two locks:
|
|
tuning_lock — guards physics-loop parameter updates (decay slope, window)
|
|
dict_lock — guards dictionary writes (word definitions, SMUDGE, REVEAL)
|
|
|
|
Modelled as first-class vm_state fields of type lock_state
|
|
(defined in StarForth_Base as: LockFree | LockHeld nat).
|
|
|
|
Safety property: mutual exclusion — at most one thread holds a lock.
|
|
Since StarForth has exactly two threads (exec + heartbeat), thread IDs
|
|
are 0 (ExecThread) and 1 (HeartbeatThread).
|
|
======================================================================== *)
|
|
|
|
(* =========================================================================
|
|
Section 1: Thread identifiers
|
|
======================================================================== *)
|
|
|
|
definition EXEC_THREAD :: nat where "EXEC_THREAD = 0"
|
|
definition HEARTBEAT_THREAD :: nat where "HEARTBEAT_THREAD = 1"
|
|
|
|
(* All valid thread IDs *)
|
|
definition valid_thread :: "nat \<Rightarrow> bool" where
|
|
"valid_thread t \<longleftrightarrow> t = EXEC_THREAD \<or> t = HEARTBEAT_THREAD"
|
|
|
|
lemma threads_distinct: "EXEC_THREAD \<noteq> HEARTBEAT_THREAD"
|
|
by (simp add: EXEC_THREAD_def HEARTBEAT_THREAD_def)
|
|
|
|
(* =========================================================================
|
|
Section 2: Lock operations
|
|
======================================================================== *)
|
|
|
|
(* acquire_lock t s: thread t acquires lock in state s.
|
|
Precondition: lock is free (s = LockFree).
|
|
Result: lock held by t. *)
|
|
definition acquire_lock :: "nat \<Rightarrow> lock_state \<Rightarrow> lock_state" where
|
|
"acquire_lock t s = (case s of LockFree \<Rightarrow> LockHeld t | LockHeld h \<Rightarrow> LockHeld h)"
|
|
|
|
(* release_lock t s: thread t releases lock in state s.
|
|
Precondition: lock held by t (s = LockHeld t).
|
|
Result: lock free. *)
|
|
definition release_lock :: "nat \<Rightarrow> lock_state \<Rightarrow> lock_state" where
|
|
"release_lock t s = (case s of LockFree \<Rightarrow> LockFree | LockHeld h \<Rightarrow> (if h = t then LockFree else LockHeld h))"
|
|
|
|
(* is_free, is_held predicates *)
|
|
definition lock_free :: "lock_state \<Rightarrow> bool" where
|
|
"lock_free s \<longleftrightarrow> s = LockFree"
|
|
|
|
definition lock_held_by :: "nat \<Rightarrow> lock_state \<Rightarrow> bool" where
|
|
"lock_held_by t s \<longleftrightarrow> s = LockHeld t"
|
|
|
|
(* =========================================================================
|
|
Section 3: Basic lock lemmas
|
|
======================================================================== *)
|
|
|
|
lemma acquire_when_free:
|
|
"acquire_lock t LockFree = LockHeld t"
|
|
by (simp add: acquire_lock_def)
|
|
|
|
lemma acquire_when_held_noop:
|
|
"acquire_lock t (LockHeld h) = LockHeld h"
|
|
by (simp add: acquire_lock_def)
|
|
|
|
lemma release_own_lock:
|
|
"release_lock t (LockHeld t) = LockFree"
|
|
by (simp add: release_lock_def)
|
|
|
|
lemma release_other_lock:
|
|
assumes "h \<noteq> t"
|
|
shows "release_lock t (LockHeld h) = LockHeld h"
|
|
by (simp add: release_lock_def assms)
|
|
|
|
lemma release_free_noop:
|
|
"release_lock t LockFree = LockFree"
|
|
by (simp add: release_lock_def)
|
|
|
|
lemma acquire_then_release:
|
|
"release_lock t (acquire_lock t LockFree) = LockFree"
|
|
by (simp add: acquire_lock_def release_lock_def)
|
|
|
|
(* =========================================================================
|
|
Section 4: Mutual exclusion — at most one holder
|
|
======================================================================== *)
|
|
|
|
(* A lock is in a valid state: either free or held by exactly one thread. *)
|
|
definition lock_wf :: "lock_state \<Rightarrow> bool" where
|
|
"lock_wf s \<longleftrightarrow> (case s of LockFree \<Rightarrow> True | LockHeld t \<Rightarrow> valid_thread t)"
|
|
|
|
lemma lock_wf_free [simp]: "lock_wf LockFree"
|
|
by (simp add: lock_wf_def)
|
|
|
|
lemma lock_wf_held:
|
|
assumes "valid_thread t"
|
|
shows "lock_wf (LockHeld t)"
|
|
by (simp add: lock_wf_def assms)
|
|
|
|
lemma acquire_preserves_wf:
|
|
assumes "lock_wf s" "valid_thread t"
|
|
shows "lock_wf (acquire_lock t s)"
|
|
using assms by (cases s; simp add: acquire_lock_def lock_wf_def)
|
|
|
|
lemma release_preserves_wf:
|
|
assumes "lock_wf s"
|
|
shows "lock_wf (release_lock t s)"
|
|
using assms by (cases s; simp add: release_lock_def lock_wf_def)
|
|
|
|
(* Two distinct threads cannot both hold the same lock. *)
|
|
lemma mutex_exclusive:
|
|
assumes "lock_held_by t s" "lock_held_by u s"
|
|
shows "t = u"
|
|
using assms by (cases s; simp add: lock_held_by_def)
|
|
|
|
(* =========================================================================
|
|
Section 5: VM-level lock accessors
|
|
======================================================================== *)
|
|
|
|
(* Acquire/release tuning_lock in the full vm_state record. *)
|
|
definition vm_acquire_tuning :: "nat \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
|
"vm_acquire_tuning t vm = vm\<lparr>tuning_lock := acquire_lock t (tuning_lock vm)\<rparr>"
|
|
|
|
definition vm_release_tuning :: "nat \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
|
"vm_release_tuning t vm = vm\<lparr>tuning_lock := release_lock t (tuning_lock vm)\<rparr>"
|
|
|
|
(* Acquire/release dict_lock in the full vm_state record. *)
|
|
definition vm_acquire_dict :: "nat \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
|
"vm_acquire_dict t vm = vm\<lparr>dict_lock := acquire_lock t (dict_lock vm)\<rparr>"
|
|
|
|
definition vm_release_dict :: "nat \<Rightarrow> vm_state \<Rightarrow> vm_state" where
|
|
"vm_release_dict t vm = vm\<lparr>dict_lock := release_lock t (dict_lock vm)\<rparr>"
|
|
|
|
(* Acquiring/releasing a lock does not change the data or return stacks. *)
|
|
lemma acquire_tuning_ds [simp]:
|
|
"data_stack (vm_acquire_tuning t vm) = data_stack vm"
|
|
by (simp add: vm_acquire_tuning_def)
|
|
|
|
lemma acquire_tuning_rs [simp]:
|
|
"return_stack (vm_acquire_tuning t vm) = return_stack vm"
|
|
by (simp add: vm_acquire_tuning_def)
|
|
|
|
lemma release_tuning_ds [simp]:
|
|
"data_stack (vm_release_tuning t vm) = data_stack vm"
|
|
by (simp add: vm_release_tuning_def)
|
|
|
|
lemma release_tuning_rs [simp]:
|
|
"return_stack (vm_release_tuning t vm) = return_stack vm"
|
|
by (simp add: vm_release_tuning_def)
|
|
|
|
lemma acquire_dict_ds [simp]:
|
|
"data_stack (vm_acquire_dict t vm) = data_stack vm"
|
|
by (simp add: vm_acquire_dict_def)
|
|
|
|
lemma acquire_dict_rs [simp]:
|
|
"return_stack (vm_acquire_dict t vm) = return_stack vm"
|
|
by (simp add: vm_acquire_dict_def)
|
|
|
|
lemma release_dict_ds [simp]:
|
|
"data_stack (vm_release_dict t vm) = data_stack vm"
|
|
by (simp add: vm_release_dict_def)
|
|
|
|
lemma release_dict_rs [simp]:
|
|
"return_stack (vm_release_dict t vm) = return_stack vm"
|
|
by (simp add: vm_release_dict_def)
|
|
|
|
(* Acquire-then-release restores the tuning_lock to its original value
|
|
(assuming the lock was free before acquisition). *)
|
|
lemma tuning_lock_round_trip:
|
|
assumes "tuning_lock vm = LockFree"
|
|
shows "tuning_lock (vm_release_tuning t (vm_acquire_tuning t vm)) = LockFree"
|
|
by (simp add: vm_acquire_tuning_def vm_release_tuning_def acquire_lock_def release_lock_def assms)
|
|
|
|
(* =========================================================================
|
|
Section 6: Well-formedness of VM lock state
|
|
======================================================================== *)
|
|
|
|
definition vm_locks_wf :: "vm_state \<Rightarrow> bool" where
|
|
"vm_locks_wf vm \<longleftrightarrow>
|
|
lock_wf (tuning_lock vm) \<and>
|
|
lock_wf (dict_lock vm)"
|
|
|
|
lemma vm_locks_wf_initial:
|
|
assumes "tuning_lock vm = LockFree"
|
|
assumes "dict_lock vm = LockFree"
|
|
shows "vm_locks_wf vm"
|
|
by (simp add: vm_locks_wf_def assms)
|
|
|
|
end
|