Is TLA spec shorter than code?

[zll zbw]

Hey guys, I wrote a spec for my cache algorithm, in which I cache data per id in memory after the first read from DB.

There're two parts in my spec, part 1 is the core algorithm for handling data update and deletion in cache of my server, as well as cache expiration. part 2 is a mimic of client and DB. Each part contributed about 200 lines in the final spec.

While in the actual program, the core algorithm, as specified in part 1 of my spec, only takes 200 lines too. I also not able to think abstractly of the algorithm, because to make it right and to explore all state spaces, I have to cover every detail of the algorithm.

So my problem/question is how could TLA spec be both shorter and less detailed than the actual program.

Things that I think I did abstractly is the mimic of request/response from/to DB and client using sequence, but in actual code, the request/response code are well encapsulated, so I also only need one line for them. I think also specified cache expiration abstractly, but I don't have to write it in the actual program, since it's in a library already.

I attached the spec, please help point out where I did wrong. Thanks!

[Hillel Wayne]

It could just be inexperience. I can't go through the whole spec for you, but one thing that I notice is you have

IsValidData(d) == d /= NULL /\ d.id \in Nat /\ d.value \in Nat /\ d.version <= MaxVersion
TypeInvariant ==
    /\ \/ UpdateRequestQueue = <<>>
       \/ \A i \in 1..Len(UpdateRequestQueue):
          /\ UpdateRequestQueue[i].client \in Clients
          /\ IsValidData(UpdateRequestQueue[i].data)
    /\ \/ DeleteRequestQueue = <<>>
       \/ \A i \in 1..Len(DeleteRequestQueue):
          /\ DeleteRequestQueue[i].client \in Clients
          /\ IsValidData(DeleteRequestQueue[i].data)

Assuming you have no additional keys in your structs, this can be shorted to:

ValidData == [id: Nat, value: Nat, version: 1..MaxVersion]

TypeInvariant ==

    /\ UpdateRequestQueue \in Seq([client: Clients, data: ValidData])

    /\ DeleteRequestQueue \in Seq([client: Clients, data: ValidData])

Which is less than half the length and much clearer. I'd guess there are similar places you can clean up the spec.

H

--
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 https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/7fb23501-ca11-437d-9351-b5967765815f%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Amir Hossein Sayyad Abdi]

It looks like that your major challenge is to model/specify the environment of your system.

Systems interact with their environment all the time, so it is critical to specify the environment as well.

Specifying programs in TLA+ may seem hard at first, because programming languages offer a rich set of APIs that act as an interface to the environment.

It is possible that your spec will be as large as your program (or even larger), because it looks like your spec needs to cover too many details. It looks like that you are not only interested in the algorithm inside your the program, but also in the implementation details as well.

I still think that if you specify the essence of your program carefully then it would be unlikely for your spec to be larger than your program.

AmirHossein

--

[Leslie Lamport]

You should not expect a TLA+ specification of a program to be shorter
than the program.  Programming languages are designed to write
programs.  There's no reason a TLA+ spec that captures the meaning of
a program should  be as short as the program itself.  For example, the
program might have an assignment statement x = x+1 .  The TLA+ formula
x' = x+1 may look similar, but it's not at all the same.  For one
thing, the statement x = x+1 is supposed to throw an exception if x
is too large.  So, its TLA+ representation would have to be something
like

  IF x+1 =< MaxInt THEN x' = x+1 ELSE ...

plus a whole lot of additional math representing the actions that
describe exception handling.  On the other hand, how would you express
the TLA+ formula x' = x+1 in the programming language?  Program code
to add two arbitrary integers is not going to be simple.  (Of
course it won't be difficult if someone has aleady implemented it; but
a TLA+ spec that someone has already written isn't hard to import
either.)

Programming languages make it easy to handle the complexities of
arithmetic on a finite set of integers, and hard to do simple
arithmetic on the actual set of integers.  It's obvious why
programming language designers made that choice.  It's less obvious
why I made the opposite choice for TLA+, and most people don't

understand it.  To get a hint of the reason why TLA+ is so different

from programming languages, read the story of the OpenComRTOS project 

described here:

   https://lamport.azurewebsites.net/tla/industrial-use.html?unhideBut=hide-rtos&unhideDiv=rtos

Experienced programmers don't get a factor of 10 reduction in code
size by improving their programming; they do it by changing the way
they think.  Learning to think in terms of algorithms and high-level
concepts rather than programs and code takes time and practice.  I
learned to do it before I became a computer scientist, but it took me
25 years to figure out how to embody that kind of thinking in a
specification language.  Don't expect to learn it in a few days.

Leslie

[zll zbw]

Thanks all for your answer!

I had this impression that TLA+ spec would be way shorter than the actual program. I think that come from Newcombie's comments on this paper introducing TLA+, and it also comes from Leslie's mention on his video course that TLA+ could be short abstraction.

If I understand this correctly, Leslie's point is TLA+ may be or not be shorter than the program, since they're not comparable, but the resulting program would definitely be short than the one without TLA+ thinking applied.

I believe the above statement is true, I have heard it many times from multiple sources, the video course, the Practical TLA+ book, the papers. But I don't ever see a concrete example of how a long program is shorten and better designed by applying TLA+ abstraction. Do you mind point me to one such example ?