Skip to content

Instantly share code, notes, and snippets.

@Calvin-L

Calvin-L/FcnRcdValue.tla

Last active November 16, 2021 23:00
Show Gist options
  • Save Calvin-L/e2e9de865a9c89640c4a381738963278 to your computer and use it in GitHub Desktop.
Save Calvin-L/e2e9de865a9c89640c4a381738963278 to your computer and use it in GitHub Desktop.
Download ZIP
Demonstration of FcnRcdValue bug
Raw
FcnRcdValue.tla
---- MODULE FcnRcdValue ----
\* This spec demonstrates a bug in the `indexTbl` field of TLC's FcnRcdValue
\* class [1], circa mid-2021.
\*
\* In particular:
\* - With one thread, FcnRcdValue behaves correctly.
\* - With two or more threads, FcnRcdValue.select() may spuriously return
\* null.
\*
\* The essence of the problem is documented in GitHub issue #439 [2]. This
\* spec makes that description fully precise by providing a plausible model
\* of the JVM's behavior on the FcnRcdValue code. It also includes a possible
\* fix [3], in which `createIndex()` gets called before the FcnRcdValue can be
\* shared with other threads. With the fix, the existing synchronization in
\* FcnRcdValue can be removed. The fix can be turned on or off in this spec
\* using the boolean constant `UseCalvinsFix`.
\*
\* Suggested model parameters:
\*
\* SPECIFICATION Spec
\* CONSTANT defaultInitValue = defaultInitValue
\* CONSTANT MemorySize = 5
\* CONSTANT Threads = {A, B}
\* CONSTANT UseCalvinsFix = FALSE
\* CHECK_DEADLOCK TRUE
\*
\*
\* [1]: https://github.com/tlaplus/tlaplus/blob/0056819723bb9ecfee428e2a6246c94ee1e7df65/tlatools/org.lamport.tlatools/src/tlc2/value/impl/FcnRcdValue.java#L37
\* [2]: https://github.com/tlaplus/tlaplus/issues/439
\* [3]: https://github.com/tlaplus/tlaplus/issues/439#issuecomment-970571916
EXTENDS TLC, Sequences, Integers, FiniteSets
CONSTANTS
MemorySize,
Threads,
UseCalvinsFix
ASSUME MemorySize \in Nat
ASSUME UseCalvinsFix \in BOOLEAN
ASSUME IsFiniteSet(Threads)
\* Set of all addresses in memory. Values in memory are integers.
Addresses == 1..MemorySize
\* The shared address where `this.indexTbl` lives. The data at this address
\* is either 0 or a pointer to the index table.
indexTbl_address == 1
\* This spec doesn't model the `domain` and `values` fields directly. Instead,
\* the FcnRcdValue is defined by this "abstract" value.
AbstractValue == (0 :> 100) @@ (1 :> 200)
MinInt(S) == CHOOSE x \in S: \A y \in S: x <= y
(*
--algorithm FcnRcdValue {
variables
\* One special worker thread gets the privilege of creating and
\* fingerprinting the FcnRcdValue.
fingerprinted = FALSE,
worker_thread \in Threads,
\* Memory:
\* - main_memory is shared.
\* - Each thread has its own cache (per_thread_memory[self]).
\* - When a thread does a write, the write does not immediately
\* reach main memory; it goes into the cache and per_thread_dirty
\* is set. Later, the CPU will flush that write to main_memory.
\* - When a thread does a read, it has to wait for the data to be
\* paged in by the CPU. In this spec, the CPU can page in any bytes
\* at any time, which models how CPU operations and JVM instructions
\* can be reordered.
\* - The CPU is allowed to page-out a cache entry at any time (after
\* which it will have to be paged-in again before being read).
main_memory = [a \in Addresses |-> 0],
per_thread_memory = [t \in Threads |-> main_memory],
per_thread_paged_in = [t \in Threads |-> [a \in Addresses |-> FALSE]],
per_thread_dirty = [t \in Threads |-> [a \in Addresses |-> FALSE]],
\* Allocations: the set of allocated addresses and the last-allocated
\* address for each thread. See `alloc(...)` below.
allocated_addresses = {indexTbl_address},
last_alloc = [t \in Threads |-> 0],
\* The holder of the lock on the `FcnRcdValue`, or {} for no holder.
lock_holder = {},
\* Each thread's output from the `select(key)` call. Our main property
\* is that after a thread exits, this value equals `AbstractValue[key]`.
lookup_output = [t \in Threads |-> 0];
macro mem_read(addr, out)
{
await per_thread_paged_in[self][addr]; \* CPU is responsible for paging-in memory
out := per_thread_memory[self][addr];
}
macro mem_write(addr, value)
{
per_thread_memory[self][addr] := value;
per_thread_dirty[self][addr] := TRUE;
per_thread_paged_in[self][addr] := TRUE;
}
macro memory_barrier()
{
\* flush all writes to main memory
await \A a \in Addresses: ~per_thread_dirty[self][a];
\* wipe local cache (need to page-in values for future reads)
per_thread_paged_in[self] := [a \in Addresses |-> FALSE];
}
macro sync_acquire()
{
await lock_holder = {};
memory_barrier();
lock_holder := self;
}
macro sync_release()
{
memory_barrier();
lock_holder := {};
}
\* Allocate N contiguous addresses. Returns the first address in the
\* allocated block (by writing that address to `last_alloc[self]`). Two
\* different threads can never allocate overlapping blocks.
\*
\* This spec does not model garbage collection; once a block is allocated,
\* it stays allocated forever.
procedure alloc(size)
{
allocate:
assert size > 0;
with (a = MinInt(Addresses \ allocated_addresses)) {
with (all_addrs_in_block = a .. (a + size - 1)) {
\* make sure we don't allocate past MemorySize
await all_addrs_in_block \subseteq Addresses;
allocated_addresses := allocated_addresses \union all_addrs_in_block;
last_alloc[self] := a;
return;
};
};
}
\* Model of the body of `createIndex()`. Always creates the index.
procedure createIndex()
{
alloc_index_table:
call alloc(2);
acquire_lock1:
if (~UseCalvinsFix) { sync_acquire(); };
write_indexTbl0:
mem_write(last_alloc[self] + 0, AbstractValue[0]);
write_indexTbl1:
mem_write(last_alloc[self] + 1, AbstractValue[1]);
release_lock1:
if (~UseCalvinsFix) { sync_release(); };
acquire_lock2:
if (~UseCalvinsFix) { sync_acquire(); };
set_this_dot_indexTbl:
mem_write(indexTbl_address, last_alloc[self]);
release_lock2:
if (~UseCalvinsFix) { sync_release(); };
return;
}
\* Model of the body of `lookupIndex(key)`. Note that the index table here
\* uses perfect hashing: each key is literally an offset into the index
\* table. The real implementation uses an imperfect hashing scheme, but
\* the core algorithm is the same.
procedure lookupIndex(key)
variables
indexTbl_start;
{
read_indexTbl:
mem_read(indexTbl_address, (* OUT *) indexTbl_start);
lookup_index:
mem_read(indexTbl_start + key, (* OUT *) lookup_output[self]);
return;
}
process (worker \in Threads)
variables
key \in DOMAIN AbstractValue;
indexTbl_address_observed = 0;
{
worker_init:
\* First: the worker thread constructs and fingerprints the value.
if (self = worker_thread) {
\* ******** PROPOSED FIX ********
\* Call `createIndex()` during fingerprinting, before
\* the value is shared with other threads.
\* ******************************
if (UseCalvinsFix) {
call createIndex();
};
worker_share_value:
fingerprinted := TRUE;
memory_barrier(); \* induced by synchronization action of adding state to shared queue
};
thread_init:
await fingerprinted;
memory_barrier(); \* induced by synchronization action of removing state from shared queue
\* ***************************
\*
\* The value has been constructed, fingerprinted, enqueued, and then
\* observed by this thread.
\*
\* The rest of this code is (roughly) the body of `select(key)`.
thread_check:
mem_read(indexTbl_address, (* OUT *) indexTbl_address_observed);
if (indexTbl_address_observed /= 0) {
call lookupIndex(key);
goto thread_done;
} else {
call createIndex();
};
thread_read:
call lookupIndex(key);
thread_done:
assert lookup_output[self] = AbstractValue[key];
}
process (cpu = "cpu")
{
cpu_act:
while (TRUE) {
either {
\* Export a dirty memory address to main memory
with (thread \in Threads, a \in allocated_addresses) {
await per_thread_dirty[thread][a];
main_memory[a] := per_thread_memory[thread][a];
per_thread_dirty[thread][a] := FALSE;
};
} or {
\* Page-out an address (but only if it is not dirty)
with (thread \in Threads, a \in allocated_addresses) {
await per_thread_paged_in[thread][a];
await ~per_thread_dirty[thread][a];
per_thread_paged_in[thread][a] := FALSE;
};
} or {
\* Page-in an address.
with (thread \in Threads, a \in allocated_addresses) {
await ~per_thread_paged_in[thread][a];
per_thread_paged_in[thread][a] := TRUE;
per_thread_memory[thread][a] := main_memory[a];
};
} or {
\* CPU can idle infinitely ONLY once all threads terminate
await \A x \in Threads: pc[x] = "Done";
};
};
}
}
*)
\* BEGIN TRANSLATION (chksum(pcal) = "543a80f" /\ chksum(tla) = "58c8185d")
\* Process variable key of process worker at line 199 col 9 changed to key_
CONSTANT defaultInitValue
VARIABLES fingerprinted, worker_thread, main_memory, per_thread_memory,
per_thread_paged_in, per_thread_dirty, allocated_addresses,
last_alloc, lock_holder, lookup_output, pc, stack, size, key,
indexTbl_start, key_, indexTbl_address_observed
vars == << fingerprinted, worker_thread, main_memory, per_thread_memory,
per_thread_paged_in, per_thread_dirty, allocated_addresses,
last_alloc, lock_holder, lookup_output, pc, stack, size, key,
indexTbl_start, key_, indexTbl_address_observed >>
ProcSet == (Threads) \cup {"cpu"}
Init == (* Global variables *)
/\ fingerprinted = FALSE
/\ worker_thread \in Threads
/\ main_memory = [a \in Addresses |-> 0]
/\ per_thread_memory = [t \in Threads |-> main_memory]
/\ per_thread_paged_in = [t \in Threads |-> [a \in Addresses |-> FALSE]]
/\ per_thread_dirty = [t \in Threads |-> [a \in Addresses |-> FALSE]]
/\ allocated_addresses = {indexTbl_address}
/\ last_alloc = [t \in Threads |-> 0]
/\ lock_holder = {}
/\ lookup_output = [t \in Threads |-> 0]
(* Procedure alloc *)
/\ size = [ self \in ProcSet |-> defaultInitValue]
(* Procedure lookupIndex *)
/\ key = [ self \in ProcSet |-> defaultInitValue]
/\ indexTbl_start = [ self \in ProcSet |-> defaultInitValue]
(* Process worker *)
/\ key_ \in [Threads -> DOMAIN AbstractValue]
/\ indexTbl_address_observed = [self \in Threads |-> 0]
/\ stack = [self \in ProcSet |-> << >>]
/\ pc = [self \in ProcSet |-> CASE self \in Threads -> "worker_init"
[] self = "cpu" -> "cpu_act"]
allocate(self) == /\ pc[self] = "allocate"
/\ Assert(size[self] > 0,
"Failure of assertion at line 140, column 13.")
/\ LET a == MinInt(Addresses \ allocated_addresses) IN
LET all_addrs_in_block == a .. (a + size[self] - 1) IN
/\ all_addrs_in_block \subseteq Addresses
/\ allocated_addresses' = (allocated_addresses \union all_addrs_in_block)
/\ last_alloc' = [last_alloc EXCEPT ![self] = a]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ size' = [size EXCEPT ![self] = Head(stack[self]).size]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << fingerprinted, worker_thread, main_memory,
per_thread_memory, per_thread_paged_in,
per_thread_dirty, lock_holder, lookup_output,
key, indexTbl_start, key_,
indexTbl_address_observed >>
alloc(self) == allocate(self)
alloc_index_table(self) == /\ pc[self] = "alloc_index_table"
/\ /\ size' = [size EXCEPT ![self] = 2]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "alloc",
pc |-> "acquire_lock1",
size |-> size[self] ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "allocate"]
/\ UNCHANGED << fingerprinted, worker_thread,
main_memory, per_thread_memory,
per_thread_paged_in,
per_thread_dirty,
allocated_addresses, last_alloc,
lock_holder, lookup_output, key,
indexTbl_start, key_,
indexTbl_address_observed >>
acquire_lock1(self) == /\ pc[self] = "acquire_lock1"
/\ IF ~UseCalvinsFix
THEN /\ lock_holder = {}
/\ \A a \in Addresses: ~per_thread_dirty[self][a]
/\ per_thread_paged_in' = [per_thread_paged_in EXCEPT ![self] = [a \in Addresses |-> FALSE]]
/\ lock_holder' = self
ELSE /\ TRUE
/\ UNCHANGED << per_thread_paged_in,
lock_holder >>
/\ pc' = [pc EXCEPT ![self] = "write_indexTbl0"]
/\ UNCHANGED << fingerprinted, worker_thread,
main_memory, per_thread_memory,
per_thread_dirty, allocated_addresses,
last_alloc, lookup_output, stack, size,
key, indexTbl_start, key_,
indexTbl_address_observed >>
write_indexTbl0(self) == /\ pc[self] = "write_indexTbl0"
/\ per_thread_memory' = [per_thread_memory EXCEPT ![self][(last_alloc[self] + 0)] = AbstractValue[0]]
/\ per_thread_dirty' = [per_thread_dirty EXCEPT ![self][(last_alloc[self] + 0)] = TRUE]
/\ per_thread_paged_in' = [per_thread_paged_in EXCEPT ![self][(last_alloc[self] + 0)] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "write_indexTbl1"]
/\ UNCHANGED << fingerprinted, worker_thread,
main_memory, allocated_addresses,
last_alloc, lock_holder,
lookup_output, stack, size, key,
indexTbl_start, key_,
indexTbl_address_observed >>
write_indexTbl1(self) == /\ pc[self] = "write_indexTbl1"
/\ per_thread_memory' = [per_thread_memory EXCEPT ![self][(last_alloc[self] + 1)] = AbstractValue[1]]
/\ per_thread_dirty' = [per_thread_dirty EXCEPT ![self][(last_alloc[self] + 1)] = TRUE]
/\ per_thread_paged_in' = [per_thread_paged_in EXCEPT ![self][(last_alloc[self] + 1)] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "release_lock1"]
/\ UNCHANGED << fingerprinted, worker_thread,
main_memory, allocated_addresses,
last_alloc, lock_holder,
lookup_output, stack, size, key,
indexTbl_start, key_,
indexTbl_address_observed >>
release_lock1(self) == /\ pc[self] = "release_lock1"
/\ IF ~UseCalvinsFix
THEN /\ \A a \in Addresses: ~per_thread_dirty[self][a]
/\ per_thread_paged_in' = [per_thread_paged_in EXCEPT ![self] = [a \in Addresses |-> FALSE]]
/\ lock_holder' = {}
ELSE /\ TRUE
/\ UNCHANGED << per_thread_paged_in,
lock_holder >>
/\ pc' = [pc EXCEPT ![self] = "acquire_lock2"]
/\ UNCHANGED << fingerprinted, worker_thread,
main_memory, per_thread_memory,
per_thread_dirty, allocated_addresses,
last_alloc, lookup_output, stack, size,
key, indexTbl_start, key_,
indexTbl_address_observed >>
acquire_lock2(self) == /\ pc[self] = "acquire_lock2"
/\ IF ~UseCalvinsFix
THEN /\ lock_holder = {}
/\ \A a \in Addresses: ~per_thread_dirty[self][a]
/\ per_thread_paged_in' = [per_thread_paged_in EXCEPT ![self] = [a \in Addresses |-> FALSE]]
/\ lock_holder' = self
ELSE /\ TRUE
/\ UNCHANGED << per_thread_paged_in,
lock_holder >>
/\ pc' = [pc EXCEPT ![self] = "set_this_dot_indexTbl"]
/\ UNCHANGED << fingerprinted, worker_thread,
main_memory, per_thread_memory,
per_thread_dirty, allocated_addresses,
last_alloc, lookup_output, stack, size,
key, indexTbl_start, key_,
indexTbl_address_observed >>
set_this_dot_indexTbl(self) == /\ pc[self] = "set_this_dot_indexTbl"
/\ per_thread_memory' = [per_thread_memory EXCEPT ![self][indexTbl_address] = last_alloc[self]]
/\ per_thread_dirty' = [per_thread_dirty EXCEPT ![self][indexTbl_address] = TRUE]
/\ per_thread_paged_in' = [per_thread_paged_in EXCEPT ![self][indexTbl_address] = TRUE]
/\ pc' = [pc EXCEPT ![self] = "release_lock2"]
/\ UNCHANGED << fingerprinted, worker_thread,
main_memory,
allocated_addresses, last_alloc,
lock_holder, lookup_output,
stack, size, key,
indexTbl_start, key_,
indexTbl_address_observed >>
release_lock2(self) == /\ pc[self] = "release_lock2"
/\ IF ~UseCalvinsFix
THEN /\ \A a \in Addresses: ~per_thread_dirty[self][a]
/\ per_thread_paged_in' = [per_thread_paged_in EXCEPT ![self] = [a \in Addresses |-> FALSE]]
/\ lock_holder' = {}
ELSE /\ TRUE
/\ UNCHANGED << per_thread_paged_in,
lock_holder >>
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << fingerprinted, worker_thread,
main_memory, per_thread_memory,
per_thread_dirty, allocated_addresses,
last_alloc, lookup_output, size, key,
indexTbl_start, key_,
indexTbl_address_observed >>
createIndex(self) == alloc_index_table(self) \/ acquire_lock1(self)
\/ write_indexTbl0(self) \/ write_indexTbl1(self)
\/ release_lock1(self) \/ acquire_lock2(self)
\/ set_this_dot_indexTbl(self)
\/ release_lock2(self)
read_indexTbl(self) == /\ pc[self] = "read_indexTbl"
/\ per_thread_paged_in[self][indexTbl_address]
/\ indexTbl_start' = [indexTbl_start EXCEPT ![self] = per_thread_memory[self][indexTbl_address]]
/\ pc' = [pc EXCEPT ![self] = "lookup_index"]
/\ UNCHANGED << fingerprinted, worker_thread,
main_memory, per_thread_memory,
per_thread_paged_in, per_thread_dirty,
allocated_addresses, last_alloc,
lock_holder, lookup_output, stack, size,
key, key_, indexTbl_address_observed >>
lookup_index(self) == /\ pc[self] = "lookup_index"
/\ per_thread_paged_in[self][(indexTbl_start[self] + key[self])]
/\ lookup_output' = [lookup_output EXCEPT ![self] = per_thread_memory[self][(indexTbl_start[self] + key[self])]]
/\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]
/\ indexTbl_start' = [indexTbl_start EXCEPT ![self] = Head(stack[self]).indexTbl_start]
/\ key' = [key EXCEPT ![self] = Head(stack[self]).key]
/\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]
/\ UNCHANGED << fingerprinted, worker_thread,
main_memory, per_thread_memory,
per_thread_paged_in, per_thread_dirty,
allocated_addresses, last_alloc,
lock_holder, size, key_,
indexTbl_address_observed >>
lookupIndex(self) == read_indexTbl(self) \/ lookup_index(self)
worker_init(self) == /\ pc[self] = "worker_init"
/\ IF self = worker_thread
THEN /\ IF UseCalvinsFix
THEN /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "createIndex",
pc |-> "worker_share_value" ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "alloc_index_table"]
ELSE /\ pc' = [pc EXCEPT ![self] = "worker_share_value"]
/\ stack' = stack
ELSE /\ pc' = [pc EXCEPT ![self] = "thread_init"]
/\ stack' = stack
/\ UNCHANGED << fingerprinted, worker_thread, main_memory,
per_thread_memory, per_thread_paged_in,
per_thread_dirty, allocated_addresses,
last_alloc, lock_holder, lookup_output,
size, key, indexTbl_start, key_,
indexTbl_address_observed >>
worker_share_value(self) == /\ pc[self] = "worker_share_value"
/\ fingerprinted' = TRUE
/\ \A a \in Addresses: ~per_thread_dirty[self][a]
/\ per_thread_paged_in' = [per_thread_paged_in EXCEPT ![self] = [a \in Addresses |-> FALSE]]
/\ pc' = [pc EXCEPT ![self] = "thread_init"]
/\ UNCHANGED << worker_thread, main_memory,
per_thread_memory,
per_thread_dirty,
allocated_addresses, last_alloc,
lock_holder, lookup_output, stack,
size, key, indexTbl_start, key_,
indexTbl_address_observed >>
thread_init(self) == /\ pc[self] = "thread_init"
/\ fingerprinted
/\ \A a \in Addresses: ~per_thread_dirty[self][a]
/\ per_thread_paged_in' = [per_thread_paged_in EXCEPT ![self] = [a \in Addresses |-> FALSE]]
/\ pc' = [pc EXCEPT ![self] = "thread_check"]
/\ UNCHANGED << fingerprinted, worker_thread, main_memory,
per_thread_memory, per_thread_dirty,
allocated_addresses, last_alloc,
lock_holder, lookup_output, stack, size,
key, indexTbl_start, key_,
indexTbl_address_observed >>
thread_check(self) == /\ pc[self] = "thread_check"
/\ per_thread_paged_in[self][indexTbl_address]
/\ indexTbl_address_observed' = [indexTbl_address_observed EXCEPT ![self] = per_thread_memory[self][indexTbl_address]]
/\ IF indexTbl_address_observed'[self] /= 0
THEN /\ /\ key' = [key EXCEPT ![self] = key_[self]]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "lookupIndex",
pc |-> "thread_done",
indexTbl_start |-> indexTbl_start[self],
key |-> key[self] ] >>
\o stack[self]]
/\ indexTbl_start' = [indexTbl_start EXCEPT ![self] = defaultInitValue]
/\ pc' = [pc EXCEPT ![self] = "read_indexTbl"]
ELSE /\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "createIndex",
pc |-> "thread_read" ] >>
\o stack[self]]
/\ pc' = [pc EXCEPT ![self] = "alloc_index_table"]
/\ UNCHANGED << key, indexTbl_start >>
/\ UNCHANGED << fingerprinted, worker_thread,
main_memory, per_thread_memory,
per_thread_paged_in, per_thread_dirty,
allocated_addresses, last_alloc,
lock_holder, lookup_output, size, key_ >>
thread_read(self) == /\ pc[self] = "thread_read"
/\ /\ key' = [key EXCEPT ![self] = key_[self]]
/\ stack' = [stack EXCEPT ![self] = << [ procedure |-> "lookupIndex",
pc |-> "thread_done",
indexTbl_start |-> indexTbl_start[self],
key |-> key[self] ] >>
\o stack[self]]
/\ indexTbl_start' = [indexTbl_start EXCEPT ![self] = defaultInitValue]
/\ pc' = [pc EXCEPT ![self] = "read_indexTbl"]
/\ UNCHANGED << fingerprinted, worker_thread, main_memory,
per_thread_memory, per_thread_paged_in,
per_thread_dirty, allocated_addresses,
last_alloc, lock_holder, lookup_output,
size, key_, indexTbl_address_observed >>
thread_done(self) == /\ pc[self] = "thread_done"
/\ Assert(lookup_output[self] = AbstractValue[key_[self]],
"Failure of assertion at line 243, column 13.")
/\ pc' = [pc EXCEPT ![self] = "Done"]
/\ UNCHANGED << fingerprinted, worker_thread, main_memory,
per_thread_memory, per_thread_paged_in,
per_thread_dirty, allocated_addresses,
last_alloc, lock_holder, lookup_output,
stack, size, key, indexTbl_start, key_,
indexTbl_address_observed >>
worker(self) == worker_init(self) \/ worker_share_value(self)
\/ thread_init(self) \/ thread_check(self)
\/ thread_read(self) \/ thread_done(self)
cpu_act == /\ pc["cpu"] = "cpu_act"
/\ \/ /\ \E thread \in Threads:
\E a \in allocated_addresses:
/\ per_thread_dirty[thread][a]
/\ main_memory' = [main_memory EXCEPT ![a] = per_thread_memory[thread][a]]
/\ per_thread_dirty' = [per_thread_dirty EXCEPT ![thread][a] = FALSE]
/\ UNCHANGED <<per_thread_memory, per_thread_paged_in>>
\/ /\ \E thread \in Threads:
\E a \in allocated_addresses:
/\ per_thread_paged_in[thread][a]
/\ ~per_thread_dirty[thread][a]
/\ per_thread_paged_in' = [per_thread_paged_in EXCEPT ![thread][a] = FALSE]
/\ UNCHANGED <<main_memory, per_thread_memory, per_thread_dirty>>
\/ /\ \E thread \in Threads:
\E a \in allocated_addresses:
/\ ~per_thread_paged_in[thread][a]
/\ per_thread_paged_in' = [per_thread_paged_in EXCEPT ![thread][a] = TRUE]
/\ per_thread_memory' = [per_thread_memory EXCEPT ![thread][a] = main_memory[a]]
/\ UNCHANGED <<main_memory, per_thread_dirty>>
\/ /\ \A x \in Threads: pc[x] = "Done"
/\ UNCHANGED <<main_memory, per_thread_memory, per_thread_paged_in, per_thread_dirty>>
/\ pc' = [pc EXCEPT !["cpu"] = "cpu_act"]
/\ UNCHANGED << fingerprinted, worker_thread, allocated_addresses,
last_alloc, lock_holder, lookup_output, stack, size,
key, indexTbl_start, key_,
indexTbl_address_observed >>
cpu == cpu_act
Next == cpu
\/ (\E self \in ProcSet: \/ alloc(self) \/ createIndex(self)
\/ lookupIndex(self))
\/ (\E self \in Threads: worker(self))
Spec == Init /\ [][Next]_vars
\* END TRANSLATION
====
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment