Skip to content

Instantly share code, notes, and snippets.

@ocadaruma

ocadaruma/PerPartitionPropertyReload.cfg

Last active March 12, 2023 01:52
Show Gist options
  • Save ocadaruma/1f9e61887d3d93e8a73422065b80205f to your computer and use it in GitHub Desktop.
Save ocadaruma/1f9e61887d3d93e8a73422065b80205f to your computer and use it in GitHub Desktop.
Download ZIP
Raw
PerPartitionPropertyReload.cfg
(**********************************************)
(* Initial predicate and next-state relation. *)
(* Alternatively, you can comment out these *)
(* and use SPECIFICATION. *)
(**********************************************)
SPECIFICATION Spec
(**********************************************)
(* Specify the values of declared constants. *)
(**********************************************)
\* CONSTANT MyConstant = {0, 1}
CONSTANTS
Partitions = {1,2}
MaxConcurrency = 2
PROPERTIES EventuallyReload
(**********************************************)
(* Formulas true in every reachable state. *)
(**********************************************)
\* INVARIANT MyInvariant
(**********************************************)
(* Disable checking deadlock. *)
(**********************************************)
\* CHECK_DEADLOCK FALSE
Raw
PerPartitionPropertyReload.tla
---- MODULE PerPartitionPropertyReload ----
EXTENDS FiniteSets, Integers, Sequences, TLC
CONSTANTS
Partitions,
MaxConcurrency
(* --algorithm per_partition_property_reload
variables
currentValue = 1;
partitionStates = [p \in Partitions |-> [paused |-> FALSE]];
partitionContexts = [p \in Partitions |-> [paused |-> FALSE, pendingTasks |-> 3, concurrency |-> 1]];
reloadStates = [p \in Partitions |-> FALSE];
fair+ process subscription = "s"
variables
i = 1;
retval = {};
begin
s_update_hw:
i := 1;
s_update_hw_loop:
while i <= Cardinality(Partitions) do
with tasks \in 0..partitionContexts[i].pendingTasks do
partitionContexts[i] := [partitionContexts[i] EXCEPT!.pendingTasks = @ - tasks];
end with;
i := i + 1
end while;
s_pause_partitions:
i := 1;
retval := {};
s_pause_partitions_loop:
while i <= Cardinality(Partitions) do
if reloadStates[i] /\ ~partitionContexts[i].paused then
retval := retval \cup {i}
end if;
i := i + 1
end while;
s_pause_partitions_update:
partitionContexts := [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = TRUE] ELSE partitionContexts[p]];
partitionStates := [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = TRUE] ELSE partitionStates[p]];
s_resume_partitions:
i := 1;
retval := {};
s_resume_partitions_loop:
while i <= Cardinality(Partitions) do
if partitionContexts[i].paused then
retval := retval \cup {i}
end if;
i := i + 1
end while;
s_resume_partitions_update:
partitionContexts := [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = FALSE] ELSE partitionContexts[p]];
partitionStates := [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = FALSE] ELSE partitionStates[p]];
s_property_reload:
partitionContexts := [p \in Partitions |-> IF reloadStates[p] /\ partitionContexts[p].pendingTasks = 0
THEN [partitionContexts[p] EXCEPT!.concurrency = currentValue] ELSE partitionContexts[p]];
goto s_update_hw
end process
fair+ process property_watcher = "w"
begin
w:
if currentValue < MaxConcurrency then
currentValue := currentValue + 1;
reloadStates := [p \in Partitions |-> TRUE];
end if;
goto w
end process
end algorithm
*)
\* BEGIN TRANSLATION (chksum(pcal) = "efc37d0e" /\ chksum(tla) = "e1c65c49")
VARIABLES currentValue, partitionStates, partitionContexts, reloadStates, pc,
i, retval
vars == << currentValue, partitionStates, partitionContexts, reloadStates, pc,
i, retval >>
ProcSet == {"s"} \cup {"w"}
Init == (* Global variables *)
/\ currentValue = 1
/\ partitionStates = [p \in Partitions |-> [paused |-> FALSE]]
/\ partitionContexts = [p \in Partitions |-> [paused |-> FALSE, pendingTasks |-> 3, concurrency |-> 1]]
/\ reloadStates = [p \in Partitions |-> FALSE]
(* Process subscription *)
/\ i = 1
/\ retval = {}
/\ pc = [self \in ProcSet |-> CASE self = "s" -> "s_update_hw"
[] self = "w" -> "w"]
s_update_hw == /\ pc["s"] = "s_update_hw"
/\ i' = 1
/\ pc' = [pc EXCEPT !["s"] = "s_update_hw_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, reloadStates, retval >>
s_update_hw_loop == /\ pc["s"] = "s_update_hw_loop"
/\ IF i <= Cardinality(Partitions)
THEN /\ \E tasks \in 0..partitionContexts[i].pendingTasks:
partitionContexts' = [partitionContexts EXCEPT ![i] = [partitionContexts[i] EXCEPT!.pendingTasks = @ - tasks]]
/\ i' = i + 1
/\ pc' = [pc EXCEPT !["s"] = "s_update_hw_loop"]
ELSE /\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions"]
/\ UNCHANGED << partitionContexts, i >>
/\ UNCHANGED << currentValue, partitionStates,
reloadStates, retval >>
s_pause_partitions == /\ pc["s"] = "s_pause_partitions"
/\ i' = 1
/\ retval' = {}
/\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, reloadStates >>
s_pause_partitions_loop == /\ pc["s"] = "s_pause_partitions_loop"
/\ IF i <= Cardinality(Partitions)
THEN /\ IF reloadStates[i] /\ ~partitionContexts[i].paused
THEN /\ retval' = (retval \cup {i})
ELSE /\ TRUE
/\ UNCHANGED retval
/\ i' = i + 1
/\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_loop"]
ELSE /\ pc' = [pc EXCEPT !["s"] = "s_pause_partitions_update"]
/\ UNCHANGED << i, retval >>
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, reloadStates >>
s_pause_partitions_update == /\ pc["s"] = "s_pause_partitions_update"
/\ partitionContexts' = [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = TRUE] ELSE partitionContexts[p]]
/\ partitionStates' = [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = TRUE] ELSE partitionStates[p]]
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions"]
/\ UNCHANGED << currentValue, reloadStates, i,
retval >>
s_resume_partitions == /\ pc["s"] = "s_resume_partitions"
/\ i' = 1
/\ retval' = {}
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop"]
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, reloadStates >>
s_resume_partitions_loop == /\ pc["s"] = "s_resume_partitions_loop"
/\ IF i <= Cardinality(Partitions)
THEN /\ IF partitionContexts[i].paused
THEN /\ retval' = (retval \cup {i})
ELSE /\ TRUE
/\ UNCHANGED retval
/\ i' = i + 1
/\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_loop"]
ELSE /\ pc' = [pc EXCEPT !["s"] = "s_resume_partitions_update"]
/\ UNCHANGED << i, retval >>
/\ UNCHANGED << currentValue, partitionStates,
partitionContexts, reloadStates >>
s_resume_partitions_update == /\ pc["s"] = "s_resume_partitions_update"
/\ partitionContexts' = [p \in Partitions |-> IF p \in retval THEN [partitionContexts[p] EXCEPT!.paused = FALSE] ELSE partitionContexts[p]]
/\ partitionStates' = [p \in Partitions |-> IF p \in retval THEN [partitionStates[p] EXCEPT!.paused = FALSE] ELSE partitionStates[p]]
/\ pc' = [pc EXCEPT !["s"] = "s_property_reload"]
/\ UNCHANGED << currentValue, reloadStates, i,
retval >>
s_property_reload == /\ pc["s"] = "s_property_reload"
/\ partitionContexts' = [p \in Partitions |-> IF reloadStates[p] /\ partitionContexts[p].pendingTasks = 0
THEN [partitionContexts[p] EXCEPT!.concurrency = currentValue] ELSE partitionContexts[p]]
/\ pc' = [pc EXCEPT !["s"] = "s_update_hw"]
/\ UNCHANGED << currentValue, partitionStates,
reloadStates, i, retval >>
subscription == s_update_hw \/ s_update_hw_loop \/ s_pause_partitions
\/ s_pause_partitions_loop \/ s_pause_partitions_update
\/ s_resume_partitions \/ s_resume_partitions_loop
\/ s_resume_partitions_update \/ s_property_reload
w == /\ pc["w"] = "w"
/\ IF currentValue < MaxConcurrency
THEN /\ currentValue' = currentValue + 1
/\ reloadStates' = [p \in Partitions |-> TRUE]
ELSE /\ TRUE
/\ UNCHANGED << currentValue, reloadStates >>
/\ pc' = [pc EXCEPT !["w"] = "w"]
/\ UNCHANGED << partitionStates, partitionContexts, i, retval >>
property_watcher == w
(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
/\ UNCHANGED vars
Next == subscription \/ property_watcher
\/ Terminating
Spec == /\ Init /\ [][Next]_vars
/\ SF_vars(subscription)
/\ SF_vars(property_watcher)
Termination == <>(\A self \in ProcSet: pc[self] = "Done")
\* END TRANSLATION
EventuallyReload ==
<>[](\A p \in Partitions: partitionContexts[p].concurrency = currentValue)
\* Check reloadRequested ~> reloaded
====
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment