Composing modules written in PlusCal

[Tristan Slominski]

Hello,

My use case revolves around building systems that have high level actions like CreateTenant, StoreObject, DestroyTenant. I've been attempting to model interleaving of DestroyTenant and StoreObject to ensure that no extra objects are around after the tenant is destroyed.

To do this, I have a TLA+ module that is a model for the Store. Then I create a PlusCal module for DestroyTenant and a PlusCal module for StoreObject. But it seems very difficult to compose the generated code from the two PlusCal modules together into one Spec with one Next function (especially since both can change the shared Store, or not, so UNCHANGED becomes difficult to specify).

Originally, if I do all of this in one single module using multiple PlusCal fair processes (one for DestroyTenant and one for StoreObject), things are straightforward and it is easy to validate the model. The problem arises when I want to refactor the single module into multiple modules, for example a Destroy module containing the fair process that implements what happens when tenant is destroyed (includes deleting stuff from Store), and another module for StoreObject, which contains a fair process that implements what happens when tenant asks for an object to be stored (including putting stuff into Store).

Is there a pattern for composing multiple modules where each is generated from its own PlusCal code? I've read this thread (https://groups.google.com/forum/#!searchin/tlaplus/module%7Csort:relevance/tlaplus/P5hIPrDgcfk/QjjRKho4BwAJ) and Chapter 10 of "Specifying Systems" book, but they both seem to assume working with TLA+ directly. Am I "doing it wrong"? Should I specify everything in TLA+ in order to achieve modularity?

Cheers,

Tristan

[Ioannis Filippidis]

Hi Tristan,

I am unfamiliar with PlusCal. From some past experience trying to combine imperative
and declarative statements for specifying systems using modular specifications,
it seems to me more practical to work directly with declarative statements, in TLA+.

If both the modules and the assumptions made during their composition (for example,
an assumption about interleaving) are in TLA+, it may be easier to reason about
how they relate to each other. An additional resource to Chapter 10 that could be
useful is the paper "Conjoining specifications" by Abadi and Lamport [1].

If the modules change the same variables, then it will probably help to refer
to Section 10.4 of the TLA+ book. A question worth considering is why do you want
to decompose the specification? Are the modules going to be reused independently
of each other? Or is the purpose to organize the specification similarly to
how the components will be implemented?

If the modules are to be reused independently, then you will probably need
to write assumptions that each one makes about the other components, and
check that it satisfies some desired properties, provided that the assumptions hold.

You will also need to check that the other components satisfy the assumptions
that the component made about them, and avoid circular dependencies among them.
This type of reasoning can quickly become more difficult than writing
a single specification for the entire system.

[1] http://lamport.azurewebsites.net/pubs/pubs.html#abadi-conjoining

Best regards,
ioannis

[Leslie Lamport]

What does it mean to compose two systems?  TLA+ models an execution of a system as a sequence of atomic actions.  When systems are modeled in this way, the only general definition of the composition of two systems I know if is that it is a system whose executions are sequences of atomic actions, each of which is an action of one of the two systems.

Let Next1 and Next2 be the next-state relations of the two systems. If both systems are described with the same collection of variables then this definition of composition means that their composition has the next-state relation Next1 \/ Next2.  If each has private variables that don't appear in the other spec, as well as variables that appear in both, then one usually defines composition to mean that actions of one of the systems leaves unchanged the private variables of the other.  Their composition then has the next-state relation

   \/ Next1 /\ UNCHANGED pvars1    
   \/ Next2 /\ UNCHANGED pvars2

where pvars1 and pvars2 are the tuples of private variables of the two systems. 

Ioannis asks the right questions about why you are decomposing the specification.  I will point out that re-use of specifications should not be a concern.  Specifications are short enough that cut-and-paste is a perfectly satisfactory method of re-using a spec.  Re-use of the implementation of a specification may be important.  This means that you would like to write a specification of a component, and be able to verify the correctness of a system that uses the component looking only at the component's specification.  That problem is what the "Conjoining Specifications" paper is about. 

Leslie

 

[Tristan Slominski]

Thank you for the responses. All the details you provided have been useful and helpful in getting me better oriented around this problem. It will take me some time to integrate everything you've highlighted, but I no longer feel stuck, and can proceed in exploring the directions you've pointed me to. I will consolidate around a single PlusCal module for now, but I also have a path towards exploring how to modularize correctly if/when needed.

Cheers,

Tristan

--
You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/RCVAYanYY_o/unsubscribe.
To unsubscribe from this group and all its topics, 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.
For more options, visit https://groups.google.com/d/optout.

[Ron Pressler]

First, using plain TLA+ does make modularity easier.

Second, I think you should consider whether composing modules is really what you need. After all, specifications should be short. Modules are great for various utility and general definitions that you may want to share among different refinement levels of your spec; they're also great to demonstrate the theoretical power of TLA+; but for practical, non-research purposes (whether you use the model checker or the proof system), I've found that if you want to specify multiple functional components, composing modules may be overkill. It's better to do the following: Specify each component as a separate specification, check it, but then, in the top-level spec, instead of actually using the component modules, use a short definition that specifies the external behavior of those components at a higher level of abstraction. 

Ron