hengxin / tlaplus-at-nju-disalg

Learning [Lamport's TLA+](http://research.microsoft.com/en-us/um/people/lamport/tla/tla.html).

tlaplus-lamport-projects

Learning Lamport's TLA+ based on various tla-resources including, for example, The TLA+ Hyperbook, The "Specifying Systems" book, The TLA+ Video Course, and many research papers on TLA+.

See roadmap.

It includes:

• tlaplus-seminar
• tlaplus-resources
  • Books
  • Tutorials
  • Video Lectures
  • Use Cases
• learning-tlaplus: Code and notes for self-learning
• other-formal-methods: Other formal methods
• tlaplus-projects: Our use of TLA+

tlaplus-at-nju-disalg's Issues

Rename `AdditionalxxxOperators` Files to xxxUtils

• Rename AdditionalxxxOperators to xxxUtils

OP, OpOperators, OT: Refactor

OP, OpOperators, OT: Refactor (In branch OP-OT-Refactor)

• + Module SystemModel
  • Containing Constants and related definitions (extracted from JupiterInterface)
• + Module Op
  • Put Op-related definitions and operators in a separate module (extracted from JupiterInterface)
  • Nop == PickNone(Op) instead of Nop == PickNone(Nat) in Op

Related Issue: Issue #24 ("To Separate Common Interfaces from Implementations")

Jupiter: Refactor `Do(c)`

Jupiter: Refactor Do(c):

• In JupiterInterface: Using DoOp(_, _) as parameter
  • + DoIns(DoOp(_, _), c)
  • + DoDel(DoOp(_, _), c)
  • + DoInt(DoOp(_, _), c)
  • + RevInt(c)
  • + SRevInt
• Using DoInt(DoOp(_, _), c) in Jupiter protocols:
  • AbsJupiter
  • CJupiter
  • XJupiter
  • AJupiter (# of states)
  • AJupiterExtended

Related Issue: Issue #24 ("To Separate Common Interfaces from Implementations")

CSComm: Refactor

CSComm: Refactor

• Make CSComm a standalone/executable specification
  • + Next, Spec
• Relation with JupiterInterface
  • Duplication of Client, Server, Msg, cincoming, sincoming

Wei-jupiter-tla Project: Basic Code/File Refactor

Basic Code/File Refactor:

1. Reduce vars definitions
   • XJupiter
2. Introduce EmptySS to denote empty (2D/Compact) state space [node |-> {{}}, edge |-> {}]
   • XJupiter: in Init
   • CJupiter: in Init
   • XJupiterImplCJupiter: in Init and CJ (refinement mapping)
3. XJupiter
   • Refactor of "Local" and "Remote" definitions
4. Jupiter
   • Move xxxUtils to the library folder

AbsJupiter

AbsJupiter

• Create a new module called AbsJupiter.tla

  • Extends a new module JupiterSerial
  • Model checking test: checking TypeOK
  • Model checking test: checking CSSync
  • Model checking test: checking WLSpec
    • a new module AbsJupiterH.tla
    • checking WLSpec

• CJupiter implements AbsJupiter:

  • Create a new module called CJupiterImplAbsJupiter.tla
  • Model checking test: AbsJ!Spec

AJupiter Family: AJupiter, AJupiterExtended, AJupiterImplXJupiter

AJupiter, AJupiterExtended, AJupiterImplXJupiter:

• commXJ in which module: AJupiterExtended? or AJupiterImplXJupiter?
• AJupiterExtended to extend AJupiter
• Simplify DoEx in AJupiterExtended
• Simplify DoImpl in AJupiterImplXJupiter
• Using DoInt structure:
  • +DoOpImpl
  • +ClientPerformImpl
  • +ServerPerformImpl
• Using xFormCopCopsShift for COTs

XJupiter: `ccur[c \in Client]` and `scur[c \in Client]` can be combined into one: `cur[r \in Replica]`

Motivation:

• Cardinality(Range(scur)) = 1

Steps:

• Check Cardinality(Range(scur)) = 1
• refactor

Jupiter: xForm

Jupiter: xForm

• AbsJupiter

• CJupiter & XJupiter:

  • cur: can be simplified to cur' = [cur EXCEPT ![r] @ \cup {cop.oid}]; No need to keep track of the current node with the sixth parameter of xFormHelper (See xForm in AbsJupiter)
  • Delete parameter xcoph of xForm (it is a duplication of coph)
    • CJupiter
    • XJupiter
  • Return a record instead of a sequence in xForm (for readability)
    • CJupiter
    • XJupiter
  • Using (+) to union two state spaces in xForm
    • CJupiter
    • XJupiter
  • Modify the state space directly instead of recording the modification and integrating them later
    (Discard: In XJupiterImplCJupiter, the incremental part of state space needs to be maintained.)
    • CJupiter
    • XJupiter

• XJupiter:

  • The common of "ClientPerform" and "ServerPerform"

• Three kinds of StateSpace in Jupiter

  • + SetStateSpace
    • Used in AbsJupiter
  • GraphStateSpace (renamed from original StateSpace)
    • Used in CJupiter and XJupiter
  • + BufferStateSpace
    • + OT on operation sequence from OT
    • + xFormShift(xform, op, ops, shift)
      • Used in AJupiter and AJupiterExtended

• Rename:

  • BufferStateSpace to xFormxxx
  • Xformxx in OTtoOTxx`
  • Xform in OT to OT

Jupiter: Adding History Variable

Jupiter: Adding History Variable

Reference:

• How to introduce history variables in a modular/reusable way?@googlegroup
• Parse error: The level of the expression or operator substituted for 'Def' must be at most 0

Possible Solution: (In branch: Jupiter-History)

• Create JupiterH module, which contains the history variable list and the history collecting procedure
• Let xxJupiterH extends/instance JupiterH (Instance Level Error)

AJupiter: Check the Correctness of AJupiter

Problem: The number of states generated by AJupiter is not equal to those generated by AbsJupiter/CJupiter/XJupiter

Possible Reasons:

• Should they be equal?
  • Evidence: AJupiterExtended and AJupiterImplCJupiter also generated different numbers of states.
    Note that the number of states generated by AJupiterImplCJupiter is equal to those generated by other Jupiter protocols.
  • To test: Write a module which only describes the C/S interaction with all inner transitions as UNCHANGED

XJupiterExtended: Extend `XJupiter` by Really `EXTENDS` It

Extend XJupiter by Really EXTENDS It

• Rewrite XJupiterExtended by
  • EXTENDS XJupiter
  • Move cincomingCJ from XJupiterImplCJupiter to the new XJupiterExtended
    • cincomingCJ + sincomingCJ (not used) => commCJ

CJupiter, XJupiter, XJupiterExtended, XJupiterImplCJupiter: Performance Issues

Performance Issues:

• SRevImpl: to avoid duplicate xForm
• Combine IgnoreDir with (+)
  • Not elegant; 2D state spaces of c2ss still contains lr.
• Is IgnoreDir necessary? (See also #25)

Profiling:

• Disk IO
• Hot Methods

JupiterInterface: Integrate the C/S Interaction (i.e., Communication) in JupiterInterface

Integrate the C/S communication pattern into JupiterInterface: (Git Branch: JupiterInterface-Comm)

• + CONSTANT Msg
• Comm == INSTANCE CSComm
• TypeOKInt
  • + Comm!TypeOK
• InitInt
  • + Comm!Init
• DoInt(DoOp, c)
  • + Comm!Send (Cancelled: It is the replicas that decide what messages to send; in DoOp)
• + CRevInt(ClientPerformInt, c)
  • + /\ Comm!CRev(c) /\ ClientPerform(c, Head(cincoming[c]))
• + SRevInt(ServerPerformInt, c)
  • + /\ Comm!SRev /\ ServerPerform(Head(sincoming))
• Jupiter protocols:
  • AbsJupiter
  • CJupiter
  • XJupiter
  • AJupiter

XJupiterImplCJupiter: Symmetry Sets in Models

Questions to Resolve:

1. Is it OK to use "Symmetry Sets" in models of AJupiter, XJupiter, and CJupiter?

   • Priority == CHOOSE f \in [Client -> 1 .. ClientNum] : Injective(f) has used CHOOSE

   My Question @ tlaplus-googlegroup:

   • Is it correct to use symmetry set in this spec?

   References:

   • When to/not to use symmetry sets? @ tlaplus-googlegroup By Stephan Merz
   • Broken symmetry due to CHOOSE f \in [S -> T] @ tlaplus-googlegroup By Ron Pressler

2. XJupiterImplCJupiter without symmetry sets generates much more states and takes mucccccccch more time.
   References:

   • The effect of symmetry sets on TLC performance @ tlaplus-googlegroup By Ron Pressler

3. Symmetry set for combined "Client" and "Priority"?

Jupiter: To Separate Common Interfaces from Implementations

To Separate Common Interfaces from Implementations

• Create a new module called JupiterInterface, which represents the interface between Jupiter system and its environment. Used in ALL Jupiter protocols: AbsJupiter, CJupiter, XJupiter, and AJupiter. The module contains:
  • Common CONSTANTS to the Jupiter family
  • Common VARIABLES to the Jupiter family
    • state
    • chins
  • Communication (providing one incoming channel for each replica) [Transfer to #48]
    • cincoming and rincoming
    • Maybe using the technique of parameterized INSTANCE
    • Shortcomings: Don't know how to express TypeOK and Init of CSComm in JupiterInterface
  • vars
  • TypeOKInt
    • state
    • chins
    • cincoming and rincoming [Transfer to #48]
  • InitInt
    • state
    • chins
    • cincoming and rincoming [Transfer to #48]
  • BIG TODO: IntDo(c) (Transfer to Issue #45)
    • How to generate ops from outside so that Do(c) can be extracted to JupiterInterface?
• Create a new module called JupiterCtx, containing the context-related info.
  Used in AbsJupiter, CJupiter, and XJupiter.
  • Oid, Cop, COT(lcop, rcop)
  • cseq (together with Oid == [c: Client, seq: Nat])
    • AbsJupter extends JupiterCtx
    • CJupiter extends JupiterCtx
    • XJupiter extends JupiterCtx
  • ds: document state
    • UpdateDS in DoCtx
    • AbsJupter extends JupiterCtx
    • CJupiter extends JupiterCtx
    • XJupiter extends JupiterCtx
• Create a new module called JupiterSerial, containing the serialization order info. at the server.
  Used in AbsJupiter and CJupiter.
  • serial, cincomingSerial, sincomingSerial
  • JupiterSerial extends JupiterCtx
  • AbsJupiter extends JupiterSerial
  • CJupiter extends JupiterSerial
  • Let XJupiterExtended extend JupiterSerial

Reference: Implementing and Combining Specifications, by Leslie Lamport, 2004.

Jupiter: Each client is responsible for ignoring the messages/operations generated by itself

Description:
The server broadcasts messages to all clients.
Each client is responsible for ignoring the messages generated by itself.

• CSComm: +SSend(msg)
• Jupiter: Rev(c): ignoring the message generated by c

Advantages:

• clean code

Disadvantages:

• larger state space

XJupiter, XJupiterImplCJupiter: Replace 'seq' by 'set' in xForm

XJupiter, XJupiterImplCJupiter: Replace 'seq' by 'set' in xForm

• XJupiter: xForm, ServerPerform, ClientPerform need to be modified
  • Model checking
• XJupiterImplCJupiter: SRevImpl needs to be modified
  • Model checking

XJupiterImplCJupiter: the `css` part of the refinement mapping is wrong

Description:
The css part of the refinement mapping is wrong.

css <- [r \in Replica |-> 
            IF r = Server 
            THEN IgnoreDir(SetReduce((+), Range(s2ss), [node |-> {{}}, edge |-> {}])) 
            ELSE IgnoreDir(c2ss[r]) (+) cxss[r]], 

Specifically, the css[c \in Client] part is wrong.

Cause:

• cxss[c] loses the information that which part of c2ss is produced by transforming which operation.
• It is not the right time to integrate cxss[c] into c2ss[c] at SRevImpl. It is too early.

Solution (Basic Idea):

• remove cxss
• add op2ss: a (global for all clients) function from op to part of c2ss
• add c2ssX: c2ssX[c]: redundant (eXtra) 2D state space maintained for client c \in Client
• In the refinement mapping: using c2ssX

Materials:

• The wrong refinement mapping:
  

• The wrong cxss:
  

• Error trace which failed at SRevImpl:
  

CJupiter&XJupiter: `ds` is redundant

Description: cur in CJupiter&XJupiter is redundant

Refactor:

• Remove cur
• cur is the largest node in CSS

Advantage:

• clean code

Disadvantage:

• high computational cost

AJupiterImplXJupiter

• Create a new module AJupiterExtended which extends AJupiter with JupiterCtx.

  • Extends JupiterCtx
  • Using Cop in Msg instead of raw op
    • Generate cop in Do(c)
  • Using Cop in cbuf and sbuf
    • Update cbuf in Do(c)
    • Update cbuf in CRev(c)
    • Update sbuf in SRev
  • Adding commXJ to simulate the channels in used XJupiter (Msg <- Seq(Cop))

• Create a new module AJupiterImplXJupiter:

  • Extends AJupiterExtended
  • INSTANCE XJupiter

There are two choices:

1. AJupiterExtended EXTENDS AJupiter
2. AJupiterExtended EXTENDS JupiterCtx.

Jupiter: Specification

Jupiter: Specification

To extract common specs in separate modules:

• EC

  • Maybe in JupiterInterface

• QC

  • Maybe in JupiterInterface

• WLSpec

  • Maybe in JupiterH

• SLSpec

  • Write and test it first
  • Maybe in JupiterH

• CSSync

• For OT

  • CP1
  • CP2

Jupiter: Refinement Structure

Jupiter: Refinement Structure

Problem:

• An even more abstract Jupiter than AbsJupiter
  • Like Consensus.tla in Paxos; also see the paper "Consensus Refined" which uses global states without message passing
  • A possible idea: the serialization order as a given info/spec.
    • serial as an impl. in AbsJupiter, CJupiter
    • ? in XJupiter
    • ? in AJupiter

JupiterInterface: How to Modify `state` in the Interface Level?

JupiterInterface: How to Modify state in the Interface Level? (Git Branch: Jupiter-History)

Note: The following refactor makes JupiterInterface executable. How to take advantage of it?

• In JupiterInterface: Using aop to modify state
  • + New variable aop[r]: the actual operation applied at replica r
  • state[r] changed by applying op[r]: + ApplyNewAop(r)
  • DoInt(c)
  • RevInt(c)
  • SRevInt
• In Jupiter protocols: Setting op' instead of modifying state directly
  • AbsJupiter
  • CJupiter
  • CJupiterImplAbsJupiter
  • XJupiter
  • XJupiterExtended
  • XJupiterImplCJupiter
  • AJupiter
  • AJupiterExtended
  • AJupiterImplXJupiter

Related Issues:

• #45 (Jupiter: Refactor Do(c))
• #24 (Jupiter: To Separate Interface)

Jupiter: Code Formatting

Jupiter: Code Formatting:

• Indentation
  • IF THEN ELSE
  • LET IN (Left Aligned)
• DoOp, ClientPerform, ServerPerform in the same logic group (Not required for all modules)
• Do(c), Rev(c), SRev in the same logic group

Jupiter: fairness requirements

Description:
To separate Do(c) from Rev(c) and SRev.
There is no requirement that the clients ever generate operations.

To Fix:

• WF_{vars}(Rev(c) \/ SRev)
• To check it

Wei-jupiter-tla Project: wiki

Wei-jupiter-tla Project: wiki

• Moving ajupiter-tla.md to wiki
• Moving the content of README.md to wiki

CJupiter and XJupter: State Space Data Structure

XJupiter: Is lr of Cop necessary?

• lr can be deduced from oid
• LOCAL and REMOTE in xForm are not necessary:
  The operation cop must be transformed with those operations that generated by different clients than the one generating cop. Therefore, we can use the condition ClientOf(cop) # ClientOf(e.cop) to choose the desired edge e.
• Delete lr of 2D state space

State Space in CJupiter and XJupiter:

• New module StateSpace.tla for this same state space representation
  • Same representation of state spaces used in CJupiter and XJupiter
    • IsSS
    • Locate
  • CJupiter extends StateSpace
  • XJupiter extends StateSpace
  • Delete IgnoreDir of XJupiterImplCJupiter

CJupiter: Replacing `sctx` and `soids` with `serial`

Refactor: To replace sctx and soids with serial

1. Problem : In CJupiter, sctx and soids are used to determine the edge ordering in CSS. sctx is a field of the Cop type.

2. Drawbacks:

   • sctxs of two operations, which are the same operation in terms of their oids, may be different. This makes the the CSSes at all replicas are not exactly the same: they are the same only when sctx are ignored. This is quite annoying.
   • XJupiter, which is considered to be equivalent to CJupiter, does not contain sctx in its Cop type.

3. Solution:

• New variable serial[r \in Replica]: the serial view of each replica about the sequence of operations received by the server.
  Advantages:

  • No "intrusive" variable in Cop and CSSes are the same as expected

  Possible Disadvantages:

  • Need another communication channel to send serial from the Server to clients
    • Indeed use another communication channel commSerial in the current solution