Wednesday, October 26, 2022

Levels of reproducibility and repeatability and replication

Knowledge progresses when one person can leverage the insights of another person. There are levels of reproducibility that require different levels investment on the part of the person looking to build on the initial knowledge. 

The levels described below are ranked from "requires lots of work to build upon" to "very easy to leverage."

Level 0: discoverable claim

Undocumented claims that no one else is aware of are irrelevant to the advancement of science. 

Level 1: claim without evidence

example: "My design for this car tire supports operational speeds of 50 miles per hour and will be usable for 50,000 miles."
No software or analytical calculations are provided. No explanation of how claim was arrived at.


Level 2: verbal hints of process used

software-based example: My design for the car tire is based on calculations from code written in Python.
analytical example: In my calculation of operational speed I used the Fourier transform.

What distinguishes 2 from 1: Advertising that code was written, or math was done. 
Most peer-reviewed scientific papers are written at this level or, if you're lucky, level 2. 
Most presentations of experiments (e.g., at conferences and lectures) also are made at this level or level 2.


Level 3: software without documentation or dependencies; or, for analytical, a few of the key equations

software-based example: Python script provided by the author to back up claim. No configuration file or random seed value. Library dependencies and versions need to be determined through trial and error (aka digital archeology).
analytical example: a few key equations (from a much more complex derivation) are mentioned, as are a few (not all) of the assumptions.

consequence: If you're smart and diligent, you may be able to recover statistically similar (though not exact) behavior for stochastic models, assuming neither you nor the original author had any bugs in the implementation.


Level 4:

software-based example: Python script with random seed value specified and configuration parameters documented. Documentation not included, nor are dependencies made explicit. 
analytical example: complete derivation provided, with explanation of assumptions

Level 5: repeatable

software-based example: Python script containerized, software versions pinned. Build process is executable. No digital archeology needed.
analytical example: portions of the complete derivation are checked by a computer algebra system (CAS) for correctness.


Level 6:

software-based example: Python script containerized with documentation of assumptions and examples of how to use. Configuration file with parameters and random seed values provided.
analytical example: complete derivation checked by a computer algebra system (CAS) for correctness. Proofs provided.  Citations where appropriate.


Caveat: the levels described above are not actually linear. There are a few meandering paths that get from 0 to 6. 


References

"Reproducibility vs. Replicability: A Brief History of a Confused Terminology"
https://www.ncbi.nlm.nih.gov/pmc/articles/PMC5778115/

Sunday, October 9, 2022

TLA+ comparison with other formal verification software

The scope of this post is limited to formal verification of algorithms and protocols. 

To save docker images to my repo,

docker pull official/imagename
docker image tag official/imagename:latest myusername/imagename:latest
docker push myusername/imagename:latest


TLA+

Check the correctness of a specification. 
Not tied to a specific implementation or tests of an implementation.

Jepsen



"Jepsen is a Clojure library. A test is a Clojure program which uses the Jepsen library to set up a distributed system, run a bunch of operations against that system, and verify that the history of those operations makes sense."

For distributed systems, introduce {partitions, added resources, removed resources, delays, clock skew} and other noises, run operations, and then compare against expected results. 

Stateright



"Stateright is a Rust actor library that aims to solve this problem by providing an embedded model checker, a UI for exploring system behavior (demo), and a lightweight actor runtime. It also features a linearizability tester that can be run within the model checker for more exhaustive test coverage than similar solutions such as Jepsen."

F*


Can generate C, as well as parser/generators. 

Not explicitly temporal (whereas TLA+ is explicitly about temporal actions), but F* could be used for temporal models.

Why3


https://why3.lri.fr/

Z3

written by the same developer as SMV after the developer moved to Microsoft

https://github.com/z3prover/z3/pkgs/container/z3

Coq

constructive dependent type theory

Lean

"Simple formally verified compiler in Lean" by Ericson (2021)

SMV

CMU's SMV --> Cadence SMV --> nuSMV

https://swmath.org/software/7795
http://mcmil.net/smv.html
https://www.cs.cmu.edu/~modelcheck/smv.html
https://sws.cs.ru.nl/publications/papers/biniam/smv/
https://web.cs.wpi.edu/~kfisler/Courses/525V/S02/Readings/smv-cadence.pdf

https://nusmv.fbk.eu/
https://en.wikipedia.org/wiki/NuSMV

Isabelle/HOL

simple type theory


Alloy


Cryptol



Spin and Promela

P

Event B

"a modelling method for formalising and developing systems whose components can be modelled as discrete transition systems. An evolution of the (classical) B-method, Event-B is now centred around the general notion of events, which are also found in other formal methods such as Action Systems, TLA and UNITY."

An Introduction to the Event-B Modelling Method

Translating B to TLA+ for Validation with TLC

https://www3.hhu.de/stups/downloads/pdf/HansenLeuschel_TLC4B_techreport.pdf

https://www.sciencedirect.com/science/article/pii/S0167642316300235

classical B for software development

https://discuss.tlapl.us/msg03080.html

Relevance of TLA+ to the Physics Derivation Graph

The Physics Derivation Graph is just a CRUD application, so I didn't expect TLA+ would be relevant. My initial view was that there isn't an algorithm or a protocol in the PDG. The PDG is just a webpage, some middleware (e.g., bash or Python) and a back-end database (CSV, SQL, JSON, Neo4j, etc). Standard MVC applies. 


After spending 1 day reviewing TLA+ materials, I realized the PDG has a workflow specification that I hadn't previously considered in detail. 

  1. User has a derivation in mind and they want to integrate it with existing PDG content. User knows their derivation's expressions, steps, symbols (variables and constants), and operators.
  2. User writes their derivation into the PDG referencing existing symbols, existing expressions, and existing inference rules. 
    • If the relevant symbol isn't available, add it.
    • If an existing symbol needs to be corrected/revised/merged, modify it.
    • If the relevant inference rule isn't available, add it.
    • If an existing inference rule needs to be corrected/revised/merged, modify it.
  3. Integrated derivation steps are checked for correctness using a Computer Algebra System (e.g., SymPy, Mathematica, etc)
That user story sounds reasonable until you consider two concurrent users editing the same steps or expressions or symbols or inference rules or operators. If each of the above steps are considered atomic, there are potential conflicts. 
  • One user could be attempting to create a new derivation step while another modifies existing symbols or inference rules. 
  • Two users could concurrently attempt to modify/merge/edit existing symbols or inference rules. When they commit their change, the thing they are changing may have disappeared or been altered.
One way to avoid the above potential for conflict would be to lock the database while edits are made (no concurrent users).
Another avoidance mechanism would be to queue changes and check consistency of every change sequentially (serialize concurrency). 

Saturday, October 8, 2022

glossary for TLA+ and PlusCal jargon

TLA+

See also TLA+ language summary and this summary. Here's another summary of operators.

jargon definition
Apalache "symbolic model checker for TLA+." "Translates TLA+ into the logic supported by SMT solvers such as Microsoft Z3."
Source: apalache github
behavior

aka execution
sequence of states
Source: Lecture 1 video

CONSTANT


Source: Specifying Systems page i25

CONSTANTS See CONSTANT
execution see behavior.
Source: Lecture 1 video
deadlock

execution stopped when it wasn't supposed to
Source: Lecture 3 video

See also termination
EXTENDS
Source: Lecture 2 video
FALSE See also TRUE
Source: Lecture 2 video
IF THEN
Source: Lecture 2 video
IF THEN ELSE
Source: Lecture 2 video
liveness property

"you have to look at the entire execution, which may be infinite, to determine that it is not satisfied."
Source: session 9

See also safety property

MODULE
Source: Lecture 2 video
PlusCal User's manual
safety property

"if is not satisfied by an execution, then you can tell that it's not satisfied by looking at a finite portion of the execution—even if the execution is infinite."
Source: session 9

See also liveness property

state assignment of values to variables
Source: Lecture 1 video and
Source: TLA+ chapter in "Software Specification Methods"
state machine, specification of
  • all possible initial states
    • variables
    • initial value of each variable
  • what state follows a given state
    • relations values of variables in current state and possible values in the next state.
Source: Lecture 1 video
state predicate

"A formula that is true or false of a state. A state predicate is just an ordinary Boolean-valued formula that can contain variables but no primed variables and no temporal operators like <>."
Source: session 9

step change from one state to the next state.
Source: Lecture 1 video
strong fairness "A step of a process is strongly fair in a behavior iff there is no point in the behavior after which the step is enabled in infinitely many states but no such step occurs in the behavior."
Source: session 9

See also weak fairness
strongly fair see strong fairness
termination

execution stopped when it was supposed to
Source: Lecture 3 video

See also deadlock
TLA

Temporal Logic of Actions
a temporal logic developed for describing and reasoning about concurrent and distributed systems
Source: Specifying and Verifying Systems With TLA+

TLAPS TLA+ proof system.
Source: Lecture 1 video and
Source: TLA+ Proof System (TLAPS)
TLA+

language for high-level modeling digital systems. Here "high-level" refers to the design aspects, above the code. Examples of digital systems: algorithms, programs, and computer systems.
Source: Lecture 1 video

"a formal specification language based on (untyped) ZF set theory, first-order logic, and TLA (the Temporal Logic of Actions)"
Source: Specifying and Verifying Systems With TLA+

TLA+ version 2 user guide (2018)

TLA+ hyperbook

TLA+ toolbox IDE for TLA+.
Source: Lecture 1 video.

Toolbox website
TLC on-the-fly model checker for debugging TLA+ specifications
Source: Specifying and Verifying Systems With TLA+
TRUE See also FALSE
Source: Lecture 2 video
VARIABLE
Source: Lecture 2 video
VARIABLES
weak fairness

the process must keep taking steps if it can
Source: session 9

See also strong fairness

weakly fair see weak fairness
/\ and
\/ or
Source: Lecture 2 video
<>

aka eventually
For any state predicate P, the formula <>P is true of a behavior iff P is true of at least one state of the behavior.
Source: session 9

[]

aka always
For any state predicate P, the formula <>P is true of a behavior iff P is true of at least one state of the behavior.
Source: session 9

~>

aka leads to
Source: session 9

' aka prime
next value


In module Sequences

See TLA+ summary page 8 of 9, and this summary.
jargon definition
Append(seq,e) the sequence obtained by appending the value e as the new last element of the sequence seq. For example,
Append(<<1, 2>>, 42) equals <<1, 2, 42>>.
Source: intermezzo 1
Head(seq) the first element of a non-empty sequence seq. For example, Head(<<"a", "c", "b">>) equals "a".
Source: intermezzo 1
\o aka concatenation
"seq1 \o seq2 is the sequence obtained by concatinating the sequences seq1 and seq2 in the obvious way. For example, seq \o <<e>> equals Append(seq,e) for any sequence seq and value e."
Source: intermezzo 1

websites for learning TLA+

Wikipedia

https://en.wikipedia.org/wiki/TLA%2B
https://news.ycombinator.com/item?id=9601770

Lamport's homepage

https://lamport.azurewebsites.net/tla/tla.html
https://lamport.azurewebsites.net/tla/learning.html
https://lamport.azurewebsites.net/video/intro.html
https://news.ycombinator.com/item?id=13918648

video tutorial series:
https://www.youtube.com/watch?v=p54W-XOIEF8&list=PLWAv2Etpa7AOAwkreYImYt0gIpOdWQevD


TLA+ Github

https://github.com/tlaplus/awesome-tlaplus

https://github.com/tlaplus/DrTLAPlus
https://github.com/tlaplus/Examples - includes DieHard4, DiningPhilosophers, Paxos,

https://github.com/dmilstein/channels

https://github.com/tlaplus-workshops/ewd998

https://github.com/Cjen1/tla_increment


LearnTLA.com - Hillel Wayne

https://learntla.com/
https://news.ycombinator.com/item?id=19661329
https://news.ycombinator.com/item?id=33010645

https://www.hillelwayne.com/post/learntla/ -- announcement about revision to book; points to learntla.com
https://news.ycombinator.com/item?id=31952643

https://hillelwayne.com/talks/distributed-systems-tlaplus/

Hillel Wayne - Designing Distributed Systems with TLA+
https://www.youtube.com/watch?v=ATobswwFwQA

Tackling Concurrency Bugs with TLA+ by Hillel Wayne
https://www.youtube.com/watch?v=_9B__0S21y8

  • toy example of money transfer in TLA+
  • three real-world cases from Hillel's employer of using TLA+ to check design before implementation


@pressron - Ron Pressler

https://pron.github.io/posts/tlaplus_part1
https://pron.github.io/posts/tlaplus_part2
https://pron.github.io/posts/tlaplus_part3
https://pron.github.io/posts/tlaplus_part4

https://pron.github.io/posts/tlaplus-curryon-talk
Ron Pressler - The Practice and Theory of TLA+
https://www.youtube.com/watch?v=15uy9Ga-14I


TLA+ in Docker in VSCode

A gentle intro to TLA+
https://www.youtube.com/watch?v=D_sh1nnX3zY
Demos a three-state system using VSCode

VSCode plug-in using Docker for TLA+:
https://github.com/kevinsullivan/TLAPlusDocker

My video on how to install TLA+ inside Docker as a plug-in for VSCode:
https://www.youtube.com/watch?v=sLGY7_agg4E


Questions and Answers

https://groups.google.com/g/tlaplus

https://stackoverflow.com/questions/tagged/tla%2b

https://www.reddit.com/r/tlaplus


Blog posts

https://elliotswart.github.io/pragmaticformalmodeling/

http://muratbuffalo.blogspot.com/2022/10/checking-statistical-properties-of.html
https://news.ycombinator.com/item?id=33077898

https://www.mydistributed.systems/2022/06/some-practical-tips-on-using-tla-and-p.html






https://roscidus.com/blog/blog/2019/01/01/using-tla-plus-to-understand-xen-vchan/
Deep dive into practical use of TLA+ for real software. Links to github repo with Dockerfile


Using TLA+ for fun and profit in the development of Elasticsearch - Yannick Welsch
https://www.youtube.com/watch?v=qYDcbcOVurc


TLA+ Toolbox for Beginners
https://www.youtube.com/watch?v=U2FAnyPygrA


Modeling Virtual Machines and Interrupts in TLA+ & PlusCal - Valentin Schneider
https://www.youtube.com/watch?v=hlLZi4wfBjs
use of TLA+ at ARM


TLA+ Tutorial 2021 at DISC 2021
https://www.youtube.com/watch?v=NXLJoUKJnDQ


Debugging software designs using testable pseudo-code (Jay Parlar)
https://www.youtube.com/watch?v=LAEXHua4MQQ
Alice and Bob money transfer model (from learntla.com)
utility: first motivating example for why TLA+ provides value to design process


A Beginner's Guide to TLA+ Exploring State Machines & Proving Correctness
https://www.youtube.com/watch?v=H7yBYoY7ILc


SREcon20 Americas - Weeks of Debugging Can Save You Hours of TLA+
https://www.youtube.com/watch?v=wjsI0lTSjIo
Uses an example written in C that has a rare deadlock.