Implementing atomic actions on decentralized data (1983)

dl.acm.org

40 points·mpweiher··7 comments

For proving distributed computing protocol soundness, I'm a big fan of formal verification and model checking, in particular TLA+[1] by Leslie Lamport who is behind the Lamport clocks referenced in the paper and curiously Latex, and the well known Byzantine generals problem in blockchains.

In particular a peer-reviewed on synchronization protocol has been proven incorrect on a subtle race condition using formal verification.

[1]: https://lamport.azurewebsites.net/tla/tla.html

Link to the PDF

http://pages.cs.wisc.edu/~remzi/Classes/739/Spring2003/Paper...

2PC ?

2-Phase-Commit protocol i.e. a scheme with "prepare-commit" and eventual rollback.

It is worth noticing that this paper presents a slightly more advanced protocol than 2PC. Relevant quote (page 21):

> The major difference is that, in our scheme, the uncommitted state of the token prevents other atomic actions from reading it.

The base 2PC protocol seems to be quite older than 1983. Arguably the first mention of 2PC in the literature is in "Notes on Data Base Operating Systems" by J. Gray (1978), and even that paper is "a compendium of data base management operating systems folklore".

Yes I know what it is lol. I was asking if the paper just introduces that.

Did they really paywall a paper from 1983?

Reply on news.ycombinator.com