admin/yugr-Implib
1
0
Fork 0
mirror of https://github.com/yugr/Implib.so synced 2026-06-08 18:33:41 +00:00
Code Issues Packages Projects Releases Wiki Activity

Assert that shim table is initialized.

Browse Source
This commit is contained in:
Yury Gribov
2025-01-26 10:46:13 +03:00
parent 0d8e97bf14
commit 916fe17f67
1 changed files with 5 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
specs/Init.tla
+5 -1
View File
@@ -91,11 +91,15 @@ LoadBeforeUse2 ==
\* Library handle set only if library is loaded (not necessarily initialized) \* Library handle set only if library is loaded (not necessarily initialized)
LibHandleCorrectness == lib_handle => lib_state \in {"LOADING", "LOADED"} LibHandleCorrectness == lib_handle => lib_state \in {"LOADING", "LOADED"}
\* All threads terminate, lock is released and library is loaded
Termination == <>[] Termination == <>[]
\* All threads terminate
/\ \A t \in THREADS : Len(threads[t]) = 0 /\ \A t \in THREADS : Len(threads[t]) = 0
\* Lock is released
/\ rec_lock.owner = NoThread /\ rec_lock.count = 0 /\ rec_lock.owner = NoThread /\ rec_lock.count = 0
\* Library is loaded
/\ lib_state = "LOADED" /\ lib_handle /\ lib_state = "LOADED" /\ lib_handle
\* Some shims resolved
/\ \E fun \in FUNS : shim_table[fun]
\* Library never UN-loaded \* Library never UN-loaded
NoLibResets == NoLibResets ==