TLC simulation error with liveness properties

[Catalin Marinas]

Hi,

I'm working on a model that tries to simulate thread priorities (spec below) and while the TLC model checking works fine, the -simulate run fails with an weird error: 'Attempted to apply EXCEPT construct to the string "prio_en"' (it looks to me like a TLC bug but I may be tripping over some unsupported feature). It always fails after the maximum simulation depth. Removing the liveness properties from .cfg works fine. Note that full checking always succeeds.

Thanks,

Catalin

------------------------------ MODULE preempt ---------------------------------

EXTENDS Naturals, Sequences, FiniteSets, TLC

CONSTANTS PROCS, PRIORITY_LEVELS

Threads == PROCS \X (1..PRIORITY_LEVELS)

(* --algorithm preempt {

variables

current_prio = [t \in PROCS |-> 1];

worked = [p \in Threads |-> FALSE];

define {

ProcId(self) == self[1]

Priority(self) == self[2]

Enabled(self) == Priority(self) >= current_prio[ProcId(self)]

TypeInv == /\ current_prio \in [PROCS -> 1..PRIORITY_LEVELS]

   /\ worked \in [Threads -> BOOLEAN]

Worked == <>(\A t \in Threads : worked[t])

}

macro prio_enter(prio) {

prio := current_prio[ProcId(self)]; \* save current priority

current_prio[ProcId(self)] := Priority(self); \* set the thread's priority

}

macro prio_exit(prio) {

current_prio[ProcId(self)] := prio; \* restore priority

}

fair+ process (t \in Threads)

variable priority;

{

start:

while (TRUE) {

prio_en: await Enabled(self);

prio_enter(priority);

work: await Enabled(self);

worked[self] := TRUE;

prio_ex: await Enabled(self);

prio_exit(priority);

}

}

} *)

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

SPECIFICATION Spec

CONSTANT defaultInitValue = defaultInitValue

\* Add statements after this line.

CONSTANTS PROCS = {p1, p2}

  PRIORITY_LEVELS = 2

INVARIANTS TypeInv

PROPERTIES Worked

[valentin....@arm.com]

Hi,

I've hit what seems to be the exact same problem on a different Spec.

I modified your preempt example to try and pinpoint the issue:

----- MODULE simulate_bug -----
EXTENDS Naturals, TLC

CONSTANTS
TASK_NAME,
CPUS

TASKS == {TASK_NAME} \X CPUS

(* --algorithm test {
variables
var = [v \in TASKS |-> 0];
define {
Worked == <>(\A t \in TASKS : var[t] = 1)
}

fair process (task \in TASKS)
{
init: var[self] := 0;
none: skip;
work: var[self] := 1;
}

} *)
=====
SPECIFICATION Spec

CONSTANTS CPUS = {cpu0}
TASK_NAME = task0

PROPERTIES Worked

$> java tlc2.TLC -simulate simulate_bug.tla
Error: TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException
: Attempted to apply EXCEPT construct to the string "none".

It seems the error only arises when all of the following conditions are met:
* The liveness property involves <>. I don't hit the bug if e.g. Worked == [](\A t \in TASKS : var[t] < 2)
* Each ProcSet element is a tuple

The Spec I'm working on (with which I hit the problem) meets those conditions.

As a sidenote, the error message is always of the shape 'Attempted to apply EXCEPT construct to the string "<label>"' where <label> is the SECOND label in the process for some reason.

[Markus Kuppe]

On 23.05.2018 16:12, valentin....@arm.com wrote:
> It seems the error only arises when all of the following conditions are met:
> * The liveness property involves <>. I don't hit the bug if e.g. Worked == [](\A t \in TASKS : var[t] < 2)

Hi Valentin,

that's a red herring. Changing diamond to box turns the liveness
property into an invariant. Invariants get verified with a different
algorithm.

ProcSet being a tuple indeed appears to be the root cause. I created an
issue [1] and attached a condensed test spec.

Thanks
Markus

[1] https://github.com/tlaplus/tlaplus/issues/164

[valentin....@arm.com]

Hi Markus,

On Wednesday, May 23, 2018 at 4:15:14 PM UTC+1, Markus Alexander Kuppe wrote:
>
> Hi Valentin,
>
> that's a red herring. Changing diamond to box turns the liveness
> property into an invariant. Invariants get verified with a different
> algorithm.
>

Right, that's actually obvious now that you point it out.

> ProcSet being a tuple indeed appears to be the root cause. I created an
> issue [1] and attached a condensed test spec.
>
> Thanks
> Markus
>
> [1] https://github.com/tlaplus/tlaplus/issues/164

Thanks !