Debug variables and VIEW

[Catalin Marinas]

Hi,

I have a spec (cut-down version below) where I need to add a debug variable (cmd) to keep track of how an invariant fails. As expected, such variable increases the state space significantly while not having any other effect on the actual model. So I added a VIEW statement to the .cfg file so that 'cmd' is left out. While it indeed decreases the state space, it still doesn't go all the way to the no debug variable case.

TLC2 Version 2.13 of 18 July 2018

Without the 'cmd' debug variable (or cmd only set to inst[1] in the spec below, which is part of the symmetry optimisation):

5369 states generated, 244 distinct states found

With the debug variable and VIEW set to cpu_vars:

10341 states generated, 470 distinct states found

With the debug variable and default view:

32935 states generated, 1497 distinct states found

Is there anything I miss? Please note that I run TLC on the command line (I couldn't find an ARM build of the Toolbox ;)).

Thank you,

Catalin

-------------------------- MODULE CPU ----------------------------------------
EXTENDS Sequences, TLC

CONSTANTS REGS,  \* the set of CPU registers (e.g. {r1, r2})
          ADDRS, \* the set of memory addresses (e.g. {a1, a2})
          DATA   \* the set of primitive data values (e.g. {d1, d2})

\* Zero data value (other than ADDRS or DATA)
Zero == CHOOSE val : val \notin ADDRS \cup DATA

\* TLC symmetry optimisations
Perms ==
  Permutations(REGS) \cup Permutations(ADDRS) \cup Permutations(DATA)

VARIABLES regs, \* CPU registers
  mem,          \* memory (virtual)
  exception,    \* exception status
  cmd           \* last executed command (debug)

cpu_vars == << regs, mem, exception >>

(* A memory location can store ADDRS or DATA or Zero *)
VALUES == ADDRS \cup DATA \cup {Zero}

CPUTypeOK ==
  /\ regs \in [REGS -> VALUES]
  /\ mem \in [ADDRS -> VALUES]
  /\ exception \in BOOLEAN

(* Registers and memory are initialised to Zero *)
CPUInit ==
  /\ regs = [r \in REGS |-> Zero]
  /\ mem = [a \in ADDRS |-> Zero]
  /\ exception = FALSE
  /\ cmd = << >>

(* Executable CPU instructions *)

(* Move an immediate value to a register *)
MOVI(reg, imm) ==
  /\ regs' = [regs EXCEPT ![reg] = imm]
  /\ UNCHANGED << mem, exception >>

(* Move the value of a register to another *)
MOV(regt, regm) ==
  /\ regs' = [regs EXCEPT ![regt] = regs[regm]]
  /\ UNCHANGED << mem, exception >>

(* Load a value from memory at the address specified by regm into
   regt. If the access is not permitted (invalid pointer), set the
   exception state *)
LDR(regt, regm) ==
  /\ LET pointer == regs[regm]
     IN  IF pointer \in ADDRS
         THEN /\ regs' = [regs EXCEPT ![regt] = mem[pointer]]
              /\ UNCHANGED exception
         ELSE /\ exception' = TRUE
              /\ UNCHANGED regs
  /\ UNCHANGED mem

(* Store the value in regt to memory at the address specified by
   regm. If the access is not permitted (invalid pointer), set the
   exception state *)
STR(regt, regm) ==
  /\ LET pointer == regs[regm]
     IN  IF pointer \in ADDRS
         THEN /\ mem' = [mem EXCEPT ![pointer] = regs[regt]]
              /\ UNCHANGED exception
         ELSE /\ exception' = TRUE
              /\ UNCHANGED mem
  /\ UNCHANGED regs

(* Execute an instruction in the form << "name", arg1, arg2 >> *)
CPUExec(inst) ==
  /\ CASE inst[1] = "movi" -> MOVI(inst[2], inst[3])
       [] inst[1] = "mov"  -> MOV(inst[2], inst[3])
       [] inst[1] = "ldr"  -> LDR(inst[2], inst[3])
       [] inst[1] = "str"  -> STR(inst[2], inst[3])
       [] OTHER -> Assert(FALSE, << "Unknown instruction", inst[1] >>)
  /\ cmd' = inst

------------------------------------------------------------------------------
CPUNext ==
  \/ \E reg \in REGS, imm \in VALUES : CPUExec(<< "movi", reg, imm >>)
  \/ \E regt, regm \in REGS : CPUExec(<< "mov", regt, regm >>)
  \/ \E regt, regm \in REGS : CPUExec(<< "ldr", regt, regm >>)
  \/ \E regt, regm \in REGS : CPUExec(<< "str", regt, regm >>)

CPUSpec == CPUInit /\ [][CPUNext]_<< cpu_vars, cmd >>

THEOREM CPUSpec => []CPUTypeOK
==============================================================================

\* CPU.cfg
CONSTANTS REGS = {r1, r2}
          ADDRS = {a1, a2}
          DATA = {d1, d2}
          Zero = Zero

SYMMETRY Perms

VIEW cpu_vars

SPECIFICATION CPUSpec

INVARIANTS CPUTypeOK

[Catalin Marinas]

On Monday, 5 November 2018 12:18:38 UTC, Catalin Marinas wrote:

Without the 'cmd' debug variable (or cmd only set to inst[1] in the spec below, which is part of the symmetry optimisation):

Small correction here: The inst[1] strings are not part of the symmetry optimisations (that was a different spec I had with ldr/str etc. as model constants). However, the rest is valid, if I change the last CPUNext line to cmd' = inst[1], I get only 244 distinct states, as expected. For some reason, it doesn't like the << inst[1], inst[2], inst[3] >> tuple in a variable that's not part of the VIEW (or I got the this part of TLC wrong).

Catalin

[Markus Kuppe]

On 05.11.18 04:18, Catalin Marinas wrote:

I have a spec (cut-down version below) where I need to add a debug variable (cmd) to keep track of how an invariant fails. As expected, such variable increases the state space significantly while not having any other effect on the actual model. So I added a VIEW statement to the .cfg file so that 'cmd' is left out. While it indeed decreases the state space, it still doesn't go all the way to the no debug variable case.

TLC2 Version 2.13 of 18 July 2018

Without the 'cmd' debug variable (or cmd only set to inst[1] in the spec below, which is part of the symmetry optimisation):

5369 states generated, 244 distinct states found

With the debug variable and VIEW set to cpu_vars:

10341 states generated, 470 distinct states found

With the debug variable and default view:

32935 states generated, 1497 distinct states found

Is there anything I miss? Please note that I run TLC on the command line (I couldn't find an ARM build of the Toolbox ;)).

Hi Catalin,

this is because you combine a view statement with symmetry reduction.  Can you open an enhancement request on GitHub [1]?

Thanks

Markus

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

[Catalin Marinas]

Hi Markus,

On Mon, 5 Nov 2018 at 19:40, Markus Kuppe
<tlaplus-go...@lemmster.de> wrote:
> this is because you combine a view statement with symmetry reduction. Can you open an enhancement request on GitHub [1]?

I wasn't aware of this. Does it have any other side-effects like not
checking the relevant states or it's just a performance aspect?

I'll raise an enhancement request.

--
Catalin