Skip to content

Modular PlusCal

Jump to bottom
Renato Costa edited this page Sep 5, 2018 · 15 revisions

Abstract

This page includes the current state of our Modular PlusCal specification. Modular PlusCal allows the specification writer to more clearly separate abstract and implementation-dependent details, allowing the PGo compiler to generate source code that is easy to change and enables the evolution of specification and implementation to happen at the same time.

This was originally discussed in #75.

This document describes language syntax and limitations associated with each feature.

Syntax

Modular PlusCal (MPCal) is comprised of four main features: archetypes, mapping macros, references and interleavings. MPCal algorithms are declared in .tla files as comments as below:

EXTENDS Integers, Sequeneces, TLC

CONSTANTS A, B, C

(************************
--mpcal DistributedProtocol {
\* Modular PlusCal specification
}
************************)

MPCal is compiled by PGo to vanilla PlusCal, which is turn translated to TLA+ by the TLA+ toolbox. Temporal properties and invariants can then be written as usual.

Archetypes

Archetypes describe the behavior of the processes being specified. They are declared as such:

archetype Coordinator(connection)
variables local = 10, success = FALSE; {
    l1: expression1;
    l2: expression2;
}

Archetypes look a lot like PlusCal processes (syntactically speaking). However, they differ in key aspects:

  • Archetypes have more strict scope: they can only access local variables or arguments passed in to them;
  • As a consequence, any macros called within an archetype also do not have access to global variables;
  • TLA+ operators called within an archetype must both: access no global variables; and be pure.
  • Assignments are restricted: only local variables or arguments passed as references can be assigned to (see References section for more details).

On the other hand, archetypes share some similarities with PlusCal processes:

  • Same labeling rules apply;
  • Archetypes have access to an implicit, immutable self parameter, defined when archetypes are instantiated.

Archetypes are used when processes are defined based on them: this is called instantiation:

CONSTANTS COORDINATORS, BACKUPS

variables connection = <<>>,
          backupConnection = <<>>;

process (MainCoordinator \in COORDINATORS) == instance Coordinator(connection);
process (BackupCoordinator \in BACKUPS) == instance Coordinator(backupConnection);

In the definition above, the connection variable is global in PlusCal. However, when PGo compiles an specification like the one above, only source code for archetypes is generated. Archetype parameters represent implementation-specific details that need to be filled in by the developer (oftentimes, the PGo runtime will provide most of the logic required in these implementation-specific components).

Clone this wiki locally