pluscal overhead

[Y2i]

There seems to be significant housekeeping in translated PlusCal code, especially when using procedures.  Does anyone know the average cost of this housekeeping when running TLC model checker?  By how much on average the state space that needs to be checked increases?  How does this increase affect average running time?

Thank you,

Yuri

-------------------------------- MODULE Func --------------------------------

EXTENDS Naturals, TLC, Sequences

Procs == 1..3

(*--algorithm Func

procedure Foo(x, y, z)

  variable w;

begin

  Foo1: w := x + y + z;

  Foo2: return;

end procedure

process Bar \in Procs

  variables a;

begin

    Bar1: call Foo(1,2,3);

end process

end algorithm

*)

\* BEGIN TRANSLATION

CONSTANT defaultInitValue

VARIABLES pc, stack, x, y, z, w, a

vars == << pc, stack, x, y, z, w, a >>

ProcSet == (Procs)

Init == (* Procedure Foo *)

        /\ x = [ self \in ProcSet |-> defaultInitValue]

        /\ y = [ self \in ProcSet |-> defaultInitValue]

        /\ z = [ self \in ProcSet |-> defaultInitValue]

        /\ w = [ self \in ProcSet |-> defaultInitValue]

        (* Process Bar *)

        /\ a = [self \in Procs |-> defaultInitValue]

        /\ stack = [self \in ProcSet |-> << >>]

        /\ pc = [self \in ProcSet |-> "Bar1"]

Foo1(self) == /\ pc[self] = "Foo1"

              /\ w' = [w EXCEPT ![self] = x[self] + y[self] + z[self]]

              /\ pc' = [pc EXCEPT ![self] = "Foo2"]

              /\ UNCHANGED << stack, x, y, z, a >>

Foo2(self) == /\ pc[self] = "Foo2"

              /\ pc' = [pc EXCEPT ![self] = Head(stack[self]).pc]

              /\ w' = [w EXCEPT ![self] = Head(stack[self]).w]

              /\ x' = [x EXCEPT ![self] = Head(stack[self]).x]

              /\ y' = [y EXCEPT ![self] = Head(stack[self]).y]

              /\ z' = [z EXCEPT ![self] = Head(stack[self]).z]

              /\ stack' = [stack EXCEPT ![self] = Tail(stack[self])]

              /\ a' = a

Foo(self) == Foo1(self) \/ Foo2(self)

Bar1(self) == /\ pc[self] = "Bar1"

              /\ /\ stack' = [stack EXCEPT ![self] = << [ procedure |->  "Foo",

                                                          pc        |->  "Done",

                                                          w         |->  w[self],

                                                          x         |->  x[self],

                                                          y         |->  y[self],

                                                          z         |->  z[self] ] >>

                                                      \o stack[self]]

                 /\ x' = [x EXCEPT ![self] = 1]

                 /\ y' = [y EXCEPT ![self] = 2]

                 /\ z' = [z EXCEPT ![self] = 3]

              /\ w' = [w EXCEPT ![self] = defaultInitValue]

              /\ pc' = [pc EXCEPT ![self] = "Foo1"]

              /\ a' = a

Bar(self) == Bar1(self)

Next == (\E self \in ProcSet: Foo(self))

           \/ (\E self \in Procs: Bar(self))

           \/ (* Disjunct to prevent deadlock on termination *)

              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

[Stephan Merz]

The main measure of complexity relevant in this context is the number of states that TLC needs to generate and store, and this is determined by the number of labels that appear in a PlusCal algorithm, since every label corresponds to an atomic transition. In turn, the number of labels is mostly related to the "grain of atomicity" that the modeler wishes to enforce. (However, the translation algorithm from PlusCal to TLA+ dictates certain positions that must be labeled, such as the entry point of a procedure or a loop.) The translation of procedures themselves is quite standard, based on a stack of parameters, local variables, and return address that is made explicit in the generated TLA+ specification.

For simple "straight-line" code such as your procedure Foo, you may prefer using macros or definitions rather than procedures, and these alternative constructs do not involve any overhead. Procedures are the construct of choice if you explicitly need to model their computational behavior, including possible interleaving in a parallel setting, rather than just the input-output relation of a subroutine.

Hope this helps,

Stephan

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

--

Stephan Merz

[Y2i]

Thank you Stephan.

I always thought the beauty of TLA+ is its use of math, which results in concise and easy to understand specs that can also be verified. There are no “implementation details” constructs such as loops, artificial stacks to manage (non-TLA) function calls, program counters, etc.  PlusCal brings these details back and makes them part of the spec (translated code).  If somebody is fine with TLA+ as it is, do they need PlusCal?  Is there anything so important that can be expressed in PlusCal but not in TLA+?

Thank you again,

Yuri

[Stephan Merz]

Dear Yuri,

Chris Newcombe once aptly called PlusCal the gateway drug to TLA+ ... it is a thin layer on top of TLA+ that has a more familiar syntax for programmers. Personally, I find TLA+ better suited for modeling high-level distributed algorithms. PlusCal is a step closer to (sequential or parallel) programs, and if your task is to model executions at that level, then you'll probably find that you have to worry about these "implementation details".

Best regards,

Stephan

[Leslie Lamport]

Hi Yuri,

There are two good reasons to use PlusCal instead of TLA+.

1. Most people who don't know TLA+ find PlusCal easier to understand.
This can make a big difference if you're writing something to be read
by others.  That's why I've published several algorithms in PlusCal
but I don't remember publishing one written in TLA+.

2.  Traditional multiprocess synchronization algorithms involve
control state.  I usually find it more natural to describe that
control state using PlusCal's programming-language structures rather
than explicitly introducing the pc variable.  (This applies as well to
sequential programs.)

Related to 1 is the fact that you can write f[x] := e instead of the
uglier

   f' = [f EXCEPT ![x] = e]

I believe that most uses of procedures are not the best way to express
the desired algorithm.  As Stephan suggested, if a procedure has only
a single label at the beginning, then it is almost always better to
either replace it with a macro or else define a TLA+ operator that
allows you to replace the procedure call with a simple assignment
statement.  People who are not used to programming with functional
languages often don't understand how anything computed with a loop
can easily be computed by a recursively defined TLA+ operator.

Leslie

[Y2i]

Thank you Leslie and Stephan, really appreciate your insights!