A Rewriting Logic Framework for Analyzing Isolation Anomalies in Concurrent Sagas — artifact

Companion artifact of the paper "A Rewriting Logic Framework for Analysing Isolation Anomalies in Concurrent Sagas" (submitted to Science of Computer Programming). The artifact contains a generic model of concurrent sagas in rewriting logic, written in Maude. The shared resource and the compensation strategy (blind overwrite, version-checked, commutative) are parameters. Sagas can be choreographed or orchestrated, and can follow plans of reads and writes over several resources. Lost updates and dirty reads are defined on the execution history and found by exhaustive search; a separate check tells whether the final values are correct. It includes the scripts that produce every table of the paper, the results reported in the paper, and a single entry point (reproduce.py) that reruns the analyses and compares them with the published results. A tutorial (docs/TUTORIAL.md) shows how to apply the framework to a new system. Requirements: Python 3.10+ and pip install -r requirements.txt (maude 1.6.0, which bundles Maude 3.5.1, umaudemc 0.18.1 and scipy 1.16.0). The quick reproduction takes about five minutes. Version 2.0 accompanies the second revision of the paper. It replaces version 1, whose anomaly predicates compared final values and have been superseded by history-based definitions.