Artifacts for "All in One: Design, Verification, and Implementation of SNOW-Optimal Read Atomic Transactions"

• The "lora" folder contains:

  • the Maude specifications of LORA, RAMP-Fast (RF), One-Phase Write (1PW), Faster Commit (FC), Committed Reads (CR), and ALT;
  • the transformed probabilistic models of the above six algorithms;
  • the generated distriubted Maude implementations of the above algorithms except ALT;
  • the Maude implementation of the workload generator replicated in each corresponding sub-folder;
  • the formal specifications of the consistency and performance properties replicated in each corresponding sub-folder.

• The "ext-cat" folder contains the extended CAT model checker.

• The "monitor" folder contains the Maude implementation of the monitoring mechanism.

• The "deploy" folder contains the deploying tool.