Süsteemide modelleerimine 2019/20 sügis

Checking Liveness

Liveness for the resource consumption example!

Let's start from the following solution to the resource consumption example:

------------------------------- MODULE cache -------------------------------

EXTENDS Integers, Sequences, TLC
CONSTANT ResourceCap, MaxConsumerReq

ASSUME ResourceCap > 0
ASSUME MaxConsumerReq \in 1..ResourceCap

(*--algorithm cache
variables 
  reserved = 0,
  resources_left = ResourceCap;
define
  ResourceInvariant == resources_left >= 0
end define;

process actor \in {"actor1", "actor2"}
variables
  resources_needed \in 1..MaxConsumerReq
begin
  WaitForResources:
while TRUE do
  when resources_left - reserved >= resources_needed;
  reserved := reserved + resources_needed;
  UseResources:
    while resources_needed > 0 do
      resources_left := resources_left - 1;
      resources_needed := resources_needed - 1;
      reserved := reserved - 1
    end while;
  with x \in 1..MaxConsumerReq do
    resources_needed := x;
  end with;
end while;
end process;

process time = "time"
begin
  Tick:
    resources_left := ResourceCap;
    goto Tick;
end process;
end algorithm; *)
=============================================================================

Now let's consider liveness. Let's state that the first process can eventually reach "UseResources". You can use this definition: MayAlwaysUse == <>(pc["actor1"]="UseResources").

• Create a model with ResourceCap=6 and MaxConsumerReq=2. What is the minimal fairness assumptions needed for TLA to accept this?
• Change the MaxConsumerReq to 4. Does this change anything? Why?

Peterson's algorithm

Create a new project peterson.tla. Start with the code for Dekker's algorithm that we discussed during the lecture: threads.tla. Modify this to implement Peterson's algorithm. You will find it useful to have a thread-local variable other = CHOOSE t \in Threads : t /= self.

• Run and make sure the sanity checks (AtMostOneCritical, Deadlocks, NoLiveLocks) pass.
• Make sure you have kept the outer loop (P5: goto P1 in the original code). Termination checking should fail, but the other liveness condition should succeed.
• Anticipate what happens if you change the goto into P5: goto P2.
• Now, for the most important exercise, change the liveness condition so that P5: goto P4 fails, but P5: goto P1 succeeds.

------------------------------ MODULE peterson ------------------------------

EXTENDS TLC, Integers
CONSTANT Threads

(*--algorithm peterson

variables 
  flag = [t \in Threads |-> FALSE],
  turn \in Threads;

define
OnlyOneCritical == \A t1, t2 \in Threads: pc[t1] = "CS" /\ pc[t2] = "CS" => t1 = t2
NoLiveLocks == \A t \in Threads: <>(pc[t] = "CS")
end define

fair process thread \in Threads
variable other = CHOOSE t \in Threads : t /= self
begin
  P1: skip;
  P2: skip;
  P3: skip;
  CS: skip;
  P4: skip;
  P5: goto P1
end process;

end algorithm; *)

=============================================================================

Ferryman

A classic problem in model checking is the ferryman problem... You have a ferryman, goat, cabbage, and wolf who want to cross the river. The ferryman can cross with at most one passenger. The following combination of items violate the invariant of things remaining uneaten:

1. the goat and the cabbage on the same side without ferryman
2. the goat and the wolf on the same side without ferryman

Can the ferryman transport get them all over to the other side? Or more precisely, can TLA find a way to transport them over?

Here is the spec, but you should add the temporal logic formula for a solution trace to exist. We will then ask TLA to disprove that there is a solution! (It will then give us a trace of the solution to prove us wrong...)

------------------------------ MODULE ferryman ------------------------------
goods == {"goat", "cabbage", "wolf", "ferryman"}

(* --algorithm ferryman

variables
  position = [item \in goods |-> "left"],
  current_item = "init" (*just for nicer trace!*)

define
  flip(dir) == CASE dir = "left" -> "right" [] dir = "right" -> "left"
  currentside == position["ferryman"]
  otherside == flip(currentside)
  currentside_items == {it \in goods : position[it] = currentside}

  Safe == \/ position["goat"] = position["wolf"] 
          \/ position["goat"] = position["cabbage"] 
          => position["ferryman"] = position["goat"]
  Solved == \A item \in goods : position[item] = "right"
  Solution == TRUE (* replace with your formula *)
  ThereIsNoSolution == ~Solution
end define

begin Ferry:
  while TRUE do
    with item \in currentside_items do (* picking ferryman to go alone *)
      position[item] := otherside || position["ferryman"] := otherside;
      current_item := item
    end with    
  end while

end algorithm*)
=============================================================================