STAR

STAR-based Component Model with TLA+ semantics



 

I am very excited to announce the SCM project, an open source STAR-based Component Model. SCM is derived from the TLA+ Specification Language and is the direct product of email conversations Dr. Lamport had the kindness to have with me during the month of January. 

The SCM project is open source (Apache 2.0) and is currently implemented in Java only. Javascript will be next. 

Formal methods are increasingly used in our industry to solve complex problems. For instance, the AWS team recently published this article summarizing their experience using TLA+:

Dangerous bugs turn out to be errors in design; the code faithfully implements the intended design, but the design fails to correctly handle a particular “rare” scenario. We have found that testing the code is inadequate as a method for finding subtle errors in design, as the number of reachable states of the code is astronomical. 

According to the AWS team, the key to solving that problem lies in increasing the precision of its designs. They found in the TLA+ Specification Language an ability to express all the legal behavior of the system. 

The SCM project delivers some of the semantics of TLA+ directly at the programming level (with a couple of noticeable deviations) and as such, enables a broad community of developers to harness the power of formal methods. What kind of power can you expect? Here is how the AWS teams sees the benefits of TLA+:

In industry, formal methods have a reputation for requiring a huge amount of training and effort to verify a tiny piece of relatively straightforward code, so the return on investment is justified only in safety-critical domains (such as medical systems and avionics). Our experience with TLA+ shows this perception to be wrong. At the time of this writing, Amazon engineers have used TLA+ on 10 large complex real-world systems. In each, TLA+ has added significant value, either finding subtle bugs we are sure we would not have found by other means, or giving us enough understanding and confidence to make aggressive performance optimizations without sacrificing correctness. Amazon now has seven teams using TLA+, with encouragement from senior management and technical leadership.

Just like in the case of TLA+, SCM allows you to express:

  • Safety. What the system is allowed to do. 
  • Liveness. What the system must eventually do.

Even though, SCM amounts to writing code, which could potentially be deployed in a running system (as a Component), it is not its primary intent. An SCM Component is optimized for rapidly converging to its most precise design, which in turn, may not be the highest performance implementation possible.

SCM is based on the STAR conceptual framework (State, Type, Action, Relation):

STAR framework

Fig. 1 – The STAR conceptual framework

STAR is a style where every concept we express is clearly positioned as a State, Type, Action or Relationship. STAR has applications in Strategy/Innovation, Problem/Solution Specification and today with SCM, in Programming/Verification as well. 

Combining the foundations of STAR and TLA+, I derived the following SCM Metamodel: 

Fig. 2 – The SCM Metamodel

What the model tells us is that an SCM component has a set of behaviors which is defined by a combination of States, Action, Types (and Relationships). The models deviates somewhat from TLA+ in the sense that the semantics of State (in STAR) would be called “Control State” in TLA+. In TLA+ a state is simply an assignment of variables (which is embodied by the Type) and control states appear as a variable (generally named pc) which is assigned values which are the labels of the control states. However, unlike TLA+, the Type and not the Action is responsible for the determination of the resulting state. That is why the second association between Actions and State is dashed, because it is infered, not specified. In SCM, Actions are purely functional and their results are presented to the Type which may or may not accept them, based on internal constraints. Once the Type accepts the new values, a determination of the new state is made, based on the mapping between a set of Ranges of values and States. (Control) States seem to be Ranges of values, not “assignments of values”.

This is how the model operates:

Of course, these semantics can be implemented in TLA+ but with a substantial complexity, even though the notion of “Range of Values” clearly belongs to mathematics. When the action is not in the position to deterministically determine the target state, at design time (which is a very common case), people are forced to implement a synthetic state (generatlly called “test”), which purpose is to make the the determination. This can be seen in the Factorial example of Dr. Lamport’s paper on “Computation and State Machines” (see page 12 , TLA+ definition).

Let’s explore now how we use SCM. A couple of examples are provided in the SCM repository (the Factorial and DieHard algorithms). 

Based on Dr. Lamport’s article, the design of the Factorial algorithm can be summarize as (BOLT Notation):

Note that:

  • Start is a standard action of the component model which determines the initial state of the component based on the values
  • Multiply and Set are associated to an automatic transition, i.e. as long as the control state of the system is “mult”, the multiply action is invoked automatically
  • We chose not to implement a Zero state and rather forbid any initial value which is less than one

The initialize action illustrate well the relationship between action-type-state since the resulting state can only be determined once the action has been completed. Of course the action could make that decision, but that would be an obvious and unwanted coupling between the type and the action, since the resulting state could be influenced by parameters outside the scope of the action.

It is that decoupling between action and types which confer to SCM a balanced articulation between Functional Programming (Action), Object Orientation (Types/Actions) and State Machine (State/Actions). 

The design of the component is expressed in the Component constructor’s, this is where elements of the metamodel are assembled. 

To facilitate the study of the Component’s behavior, SCM generates PlantUML activity and state diagrams both as traces of execution or after a “walk”. For instance the Factorial algorithm will generate that state diagram:

Factorial Algorithm State Diagram

Please note that the “d1” state is a desired state, not a control state. Here is corresponding PlantUML descriptor (generated by SCM):

I’d be more than honored if you would give SCM a try. If you have any question, feel free to reach me at jdubray@xgen.io

Leave a Reply

Your email address will not be published. Required fields are marked *

49 − 40 =