Random Notes/TODO

[lemmy]

TODO

• [ ] Announce the date of talk at https://github.com/tlaplus/DrTLAPlus

Notes

• Reorder commits s.t. Dijkstra's invariant IInv appears before the "optimizations"
• Animate (interesting) error traces (requires adding a history variable in EWD998 to track who gets activated by whom in the SendMsg action. In EWD998Chan, the inboxes replace the history variable)
  • v09 violated Inv with a trace of eight states
  • v04 violates Prop with a trace of six states ending in stuttering
• Consider adding a link to HOL-TLA proof: https://gist.github.com/DaveCTurner/4dbf5c4b43cd0500ff223ef1ed412b21

Statistics

• [x] Statistically quantify the effect of the "optimizations" by simulating the different spec variants (inspired by more complex SWIM spec)
• ~Add auxiliary variables to maintain stats/behavior~
• ~Note: Cannot reset TLCSet/Get performance counters in Init because simulation evaluates Init only once at startup~
• ~Fixing fingerprint seed (-seed 42) makes comparison easier~
• [x] Count the number of actions until termination is detected after termination actually occurred (how much token passing goes on until termination is eventually detected => hypothesis is that this will show the usefulness of PT1 and PT2)
• [x] PT3 optimization
• Whether changing the ratio of message passing to deactivate action changes the efficacy of the optimizations
• EWD840 is a peculiar deadlock detection algorithm => What measures/metrics are interesting for deadlock detection algorithms? See if we can collect relevant data with TLC simulation.
• Skew workloads (with e.g. RandomElement as an additional enablement condition of actions)
  • Same probability of actions is not interesting for reality
• Do not only count the number of occurrences of actions in behaviors but attach costs to actions
• Measure worst-case/tail latency
• Quantify the transition probabilities of all transitions in a state graph and see if it hints at performance bottlenecks

[lemmy]

WIP animation:

---- CONFIG EWD840_anim -----
CONSTANTS
    N = 5

SPECIFICATION 
    Spec

ALIAS
    Alias

INVARIANT 
    Inv
=====

------------------------------- MODULE EWD840_anim -------------------------------
EXTENDS EWD840, SVG, TLC, Sequences, Integers, TLCExt

color == [n \in Node |-> "white"]
history == <<1,2,"frob">>
tokenColor == IF tcolor THEN "black" ELSE "white"

---------------------------------------------------------------------------
Arial == [font |-> "Arial"]

LegendBasePos == [ x |-> -5, y |-> 25 ]

RingBasePos == [w |-> 55, h |-> 55, r |-> 75]

\* 12pts (x/y) offset to be concentric with RingNetwork.
TokenBasePos == [ w |-> RingBasePos.w + 12, 
                  h |-> RingBasePos.h + 12,
                  r |-> RingBasePos.r + 25 ]

---------------------------------------------------------------------------
\* Labels

Labels == Group(<<Text(LegendBasePos.x, LegendBasePos.y, "Circle: Active, Black: Tainted", Arial),
                  Text(LegendBasePos.x, LegendBasePos.y + 20, "Line: Message, Arrow: Receiver", Arial),
                  Text(LegendBasePos.x, LegendBasePos.y + 40, "Level: " \o ToString(TLCGet("level")), Arial)>>,
                  <<>>)

---------------------------------------------------------------------------
NodeDimension == 26

\* Ring Network
RingNetwork ==
    LET RN[ n \in Node ] ==         
            LET coord == NodeOfRingNetwork(RingBasePos.w, RingBasePos.h, RingBasePos.r, n, N)    
                id == Text(coord.x + 10, coord.y - 5, ToString(n), Arial)
                node == Rect(coord.x, coord.y, NodeDimension, NodeDimension,
                                            \* round (rx=15) if node is active.
                                            [rx |-> IF ~active[n] THEN "0" ELSE "15",
                                            stroke |-> "black", 
                                            fill |-> color[n]])
            IN Group(<<node, id>>, ("transform" :> "translate(0 125)"))
    IN Group(RN, <<>>)

---------------------------------------------------------------------------
\* Token ring (with larger radius than ring above and only for the node that currently holds the token).
TokenNetwork ==     
    LET coord == NodeOfRingNetwork(TokenBasePos.w, TokenBasePos.h, TokenBasePos.r, tpos, N)    
        circ  == Circle(coord.x, coord.y, 5, [stroke |-> "black", fill |-> tokenColor])  
    \* Group always expects a sequence!
    IN Group(<<circ>>, ("transform" :> "translate(0 125)"))

---------------------------------------------------------------------------
\* Messages send from one node to another.  A proper arrow would be more intuitive with regards to the direction
\* of message flow but SVG doesn't natively has arrows.  This is why we use a lollipop instead where the ball
\* replaces the arrowhead. 

\* Centers the line/circle at the center of a node instead of
\* a node's left upper corner (which are its 0:0 coordinates).
ArrowPosOffset == NodeDimension \div 2

Messages ==
    LET from == NodeOfRingNetwork(RingBasePos.w, RingBasePos.h, RingBasePos.r, history[1], N)
        to   == NodeOfRingNetwork(RingBasePos.w, RingBasePos.h, RingBasePos.r, history[2], N)
        line == Line(from.x + ArrowPosOffset, from.y + ArrowPosOffset, 
                        to.x + ArrowPosOffset, to.y + ArrowPosOffset, 
                        [stroke |-> "orange", marker_end |-> "url(#arrow)"])
    IN Group(IF TLCGet("action").name = "SendMsg" THEN <<line>> ELSE <<>>, ("transform" :> "translate(0 125)"))

---------------------------------------------------------------------------
\* This is just the arrow head that's used by the Message definition above as an attribute.
Defs ==
    "<defs><marker id='arrow' markerWidth='15' markerHeight='15' refX='0' refY='3' orient='auto' markerUnits='strokeWidth' viewBox='0 0 20 20'><path d='M0,0 L0,6 L9,3 z' fill='orange' /></marker></defs>"

Animation == SVGElemToString(Group(<<Labels, RingNetwork, TokenNetwork, Messages>>, <<>>))

SomeAction ==
    \* \/ tcolor # tcolor'
    \* \/ tpos # tpos'
    \/ active # active'

Alias == [ 
    action |-> TLCGet("action").name = "SendMsg",
    i |-> {i \in Node: SendMsg(i)},
    j |-> {j \in Node: active[j] # active'[j]},
    \* toolbox |-> Animation,
    eyeofgnome |-> "<svg viewBox='-80 0 300 300'>" \o Defs \o Animation \o "</svg>"
    ]

---------------------------------------------------------------------------

\* Property that leads to interesting traces when animated.

AnimInv == terminationDetected => TLCGet("level") < 20 

=============================================================================

[lemmy]

Goal of talk is to show rapid prototyping with TLA+:

1) Pass token along the ring -> InitiateProbe and PassToken actions

2) Active node passes token along, address by requiring nodes to be inactive to pass along -> Add node inactivity as enablement condition to PassToken action

3) Liveness issue because nodes might never deactivate -> Add fairness constraint that nodes eventually deactivate?

4) In a more realistic distributed system, a node j with j < i might (re-) activate node i -> Add action SendMsg to spec (no need for ReceiveMsg because of atomic message deliver and spec language)

5) Now, we need to track state, i.e., has a node send a message to a node with a higher id (we required a ring topology)