Skip to content

Commit

Permalink
add repository links
Browse files Browse the repository at this point in the history
  • Loading branch information
banhday committed Jul 30, 2018
1 parent f9dd2bf commit c32deaa
Show file tree
Hide file tree
Showing 29 changed files with 27 additions and 43 deletions.
2 changes: 1 addition & 1 deletion specifications/2PCwithBTM/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### 2PCwithBTM
#### <a href="https://github.com/muratdem/PlusCal-examples/blob/master/2PCTM/">2PCwithBTM</a>
- Specification's authors: Murat Demirbas
- Original paper: <a href="http://lamport.azurewebsites.net/tla/two-phase.html">Gray, Jim, and Leslie Lamport. Consensus on transaction commit. ACM Transactions on Database Systems (TODS) 31.1 (2006): 133-160.</a>
- Extended modules: FinSet, Int, Seq
Expand Down
2 changes: 1 addition & 1 deletion specifications/802.16/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### 802.16
#### <a href="http://list.cs.northwestern.edu/802.16/">802.16</a>
- Specification's authors: Prasad Narayana, Ruiming Chen, Yao Zhao, Yan Chen, Zhi (Judy) Fu, and Hai Zhou
- Original paper: <a href="https://ieeexplore.ieee.org/document/5062485/">802.16-2009 - IEEE Standard for Local and metropolitan area networks Part 16: Air Interface for Broadband Wireless Access Systems</a>
- Extended modules: Int, Seq, FinSet
Expand Down
8 changes: 0 additions & 8 deletions specifications/Boulangerie/README.md

This file was deleted.

2 changes: 1 addition & 1 deletion specifications/CASPaxos/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### CASPaxos
#### <a href="https://github.com/tschottdorf/caspaxos-tla">CASPaxos</a>
- Specification's authors: Tobias Schottdorf
- Original paper: <a href="http://rystsov.info/2017/02/15/simple-consensus.html">In search of a simple consensus algorithm</a>
- Extended modules: Int, FinSet
Expand Down
2 changes: 1 addition & 1 deletion specifications/Caesar/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### Caesar
#### <a href="https://github.com/nano-o/Caesar">Caesar</a>
- Specification's authors: Giuliano Losa
- Original paper: <a href="https://ieeexplore.ieee.org/document/8023110/">Arun, Balaji, et al. Speeding up Consensus by Chasing Fast Decisions. 2017 47th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN). IEEE, 2017.</a>
- Extended modules: FinSet, Seq, Int
Expand Down
8 changes: 0 additions & 8 deletions specifications/ChangRoberts/README.md

This file was deleted.

2 changes: 1 addition & 1 deletion specifications/DataPort/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### DataPort
#### <a href="https://ieeexplore.ieee.org/iel7/7858577/7862346/07862411.pdf">DataPort</a>
- Specification's authors: Geoffrey Biggs, Noriaki Ando
- Original paper: <a href="https://ieeexplore.ieee.org/iel7/7858577/7862346/07862411.pdf">Biggs, Geoffrey, and Noriaki Ando. A formal specification of the RT-Middleware data transfer protocol. Simulation, Modeling, and Programming for Autonomous Robots (SIMPAR), IEEE International Conference on. IEEE, 2016.</a>
- Extended modules: Int, Seq
Expand Down
2 changes: 1 addition & 1 deletion specifications/HLC/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### HLC
#### <a href="https://github.com/muratdem/HLC">HLC</a>
- Specification's authors: Murat Demirbas
- Original paper: <a href="https://cse.buffalo.edu/tech-reports/2014-04.pdf">Demirbas, Murat, et al. Logical Physical Clocks and Consistent Snapshots in Globally Distributed Databases. (2014).</a>
- Extended modules: Int
Expand Down
2 changes: 1 addition & 1 deletion specifications/MultiPaxos/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### MultiPaxos
#### <a href="https://github.com/nano-o/MultiPaxos">MultiPaxos</a>
- Specification's authors: Giuliano Losa
- Original paper: <a href="https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/tr-2005-33.pdf">Lamport, Leslie. Generalized Consensus and Paxos. (2004).</a>
- Extended modules: Int, FinSet
Expand Down
2 changes: 1 addition & 1 deletion specifications/SnapshotIsolation/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### SnapshotIsolation
#### <a href="https://github.com/sanjosh/tlaplus/blob/master/amazon/serializableSnapshotIsolation.tla">SnapshotIsolation</a>
- Specification's authors: Michael J. Cahill, Uwe Röhm, Alan D. Fekete
- Original paper: <a href="http://cahill.net.au/wp-content/uploads/2010/02/cahill-thesis.pdf">Cahill, Michael J., Uwe Röhm, and Alan D. Fekete. Serializable isolation for snapshot databases. ACM Transactions on Database Systems (TODS) 34.4 (2009): 20.</a>
- Extended modules: FinSet, Int, Seq
Expand Down
2 changes: 1 addition & 1 deletion specifications/SyncConsensus/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### SyncConsensus
#### <a href="https://github.com/muratdem/PlusCal-examples/tree/master/SyncConsensus">SyncConsensus</a>
- Specification's authors: Murat Demirbas
- Original paper: <a href="http://muratbuffalo.blogspot.com/2017/11/tlapluscal-modeling-of-synchronized.html">TLA+/PlusCal modeling of Synchronized Round Consensus Algorithm</a>
- Extended modules: FinSet, Int, Seq
Expand Down
2 changes: 1 addition & 1 deletion specifications/Termination/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### Termination
#### <a href="https://github.com/nano-o/Distributed-termination-detection">Termination</a>
- Specification's authors: Giuliano Losa
- Original paper: <a href="https://link.springer.com/article/10.1007/BF01782776">Mattern, Friedemann. Algorithms for distributed termination detection. Distributed computing 2.3 (1987): 161-175.</a>
- Extended modules: FinSet, Bags, Nat
Expand Down
2 changes: 1 addition & 1 deletion specifications/VoldemortKV/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### VoldemortKV
#### <a href="https://github.com/muratdem/PlusCal-examples/tree/master/VoldemortKV">VoldemortKV</a>
- Specification's authors: Murat Demirbas
- Original paper: <a href="http://www.project-voldemort.com/voldemort/">Project Voldemort - a distributed database</a>
- Extended modules: FinSet, Int, Seq
Expand Down
2 changes: 1 addition & 1 deletion specifications/acp-nb-wrong/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### acp-nb-wrong
#### <a href="https://members.loria.fr/SMerz/talks/argentina2005/Charpentier/charpov/Teaching/CS-986/TLC/">acp-nb-wrong</a>
- Specification's authors: Stephan Merz
- Original paper: <a href="https://dl.acm.org/citation.cfm?id=302436">Babaoğlu, Özalp, and Sam Toueg. Non-blocking atomic commitment. Distributed systems (2nd Ed.). ACM Press/Addison-Wesley Publishing Co., 1993.</a>
- Extended modules: default theories
Expand Down
2 changes: 1 addition & 1 deletion specifications/acp-nb/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### acp-nb
#### <a href="https://members.loria.fr/SMerz/talks/argentina2005/Charpentier/charpov/Teaching/CS-986/TLC/">acp-nb</a>
- Specification's authors: Stephan Merz
- Original paper: <a href="https://dl.acm.org/citation.cfm?id=302436">Babaoğlu, Özalp, and Sam Toueg. Non-blocking atomic commitment. Distributed systems (2nd Ed.). ACM Press/Addison-Wesley Publishing Co., 1993.</a>
- Extended modules: default theories
Expand Down
2 changes: 1 addition & 1 deletion specifications/acp-sb/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### acp-sb
#### <a href="https://members.loria.fr/SMerz/talks/argentina2005/Charpentier/charpov/Teaching/CS-986/TLC/">acp-sb</a>
- Specification's authors: Stephan Merz
- Original paper: <a href="https://dl.acm.org/citation.cfm?id=302436">Babaoğlu, Özalp, and Sam Toueg. Non-blocking atomic commitment. Distributed systems (2nd Ed.). ACM Press/Addison-Wesley Publishing Co., 1993.</a>
- Extended modules: default theories
Expand Down
2 changes: 1 addition & 1 deletion specifications/async-comm/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### async-comm
#### <a href="http://hurault.perso.enseeiht.fr/asynchronousCommunication/">async-comm</a>
- Specification's authors: Florent Chevrou, Aurélie Hurault, Philippe Quéinnec
- Original paper: <a href="https://link.springer.com/article/10.1007/s00165-016-0379-x">Chevrou, Florent, Aurélie Hurault, and Philippe Quéinnec. On the diversity of asynchronous communication. Formal Aspects of Computing 28.5 (2016): 847-879.</a>
- Extended modules: Nat
Expand Down
2 changes: 1 addition & 1 deletion specifications/byihive/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### byihive
#### <a href="https://github.com/byisystems/byihive">byihive</a>
- Specification's authors: Santhosh Raju
- Original paper: <a href="https://tools.ietf.org/rfc/rfc3506.txt">Requirements and Design for Voucher Trading System (VTS)</a>
- Extended modules: default theories
Expand Down
2 changes: 1 addition & 1 deletion specifications/diskpaxos/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### diskpaxos
#### <a href="https://github.com/nano-o/MultiPaxos/blob/master/DiskPaxos.tla">diskpaxos</a>
- Specification's authors: Giuliano Losa
- Original paper: <a href="https://lamport.azurewebsites.net/pubs/disk-paxos.pdf">Gafni, Eli, and Leslie Lamport. Disk paxos. Distributed Computing 16.1 (2003): 1-20.</a>
- Extended modules: Int
Expand Down
2 changes: 1 addition & 1 deletion specifications/egalitarian-paxos/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### egalitarian-paxos
#### <a href="https://github.com/efficient/epaxos">egalitarian-paxos</a>
- Specification's authors: Iulian Moraru
- Original paper: <a href="https://dl.acm.org/citation.cfm?id=2517350">Iulian Moraru, David G. Andersen, and Michael Kaminsky. 2013. There is more consensus in Egalitarian parliaments. In Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles (SOSP '13). ACM, New York, NY, USA, 358-372.</a>
- Extended modules: Nat, FinSet
Expand Down
2 changes: 1 addition & 1 deletion specifications/fastpaxos/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### fastpaxos
#### <a href="https://www.microsoft.com/en-us/research/publication/fast-paxos/">fastpaxos</a>
- Specification's authors: Heidi Howard
- Original paper: <a href="https://www.microsoft.com/en-us/research/publication/fast-paxos/">Lamport, Leslie. Fast paxos. Distributed Computing 19.2 (2006): 79-103.</a>
- Extended modules: Nat, FinSet
Expand Down
2 changes: 1 addition & 1 deletion specifications/fpaxos/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### fpaxos
#### <a href="https://github.com/fpaxos/fpaxos-tlaplus">fpaxos</a>
- Specification's authors: Heidi Howard
- Original paper: <a href="http://drops.dagstuhl.de/opus/volltexte/2017/7111/pdf/lipics-vol70-opodis2016-complete.pdf#page=361">Howard, Heidi, Dahlia Malkhi, and Alexander Spiegelman. Flexible Paxos: Quorum Intersection Revisited. 20th International Conference on Principles of Distributed Systems. 2017.</a>
- Extended modules: Int
Expand Down
2 changes: 1 addition & 1 deletion specifications/leaderless/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### leaderless
#### <a href="https://losa.fr/research/leaderless/">leaderless</a>
- Specification's authors: Giuliano Losa
- Original paper: <a href="https://www.ssrg.ece.vt.edu/papers/2016_podc.pdf">Losa, Giuliano, Sebastiano Peluso, and Binoy Ravindran. Brief announcement: A family of leaderless generalized-consensus algorithms. Proceedings of the 2016 ACM Symposium on Principles of Distributed Computing. ACM, 2016.</a>
- Extended modules: FinSet, Int, Seq
Expand Down
2 changes: 1 addition & 1 deletion specifications/losa_ap/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### losa_ap
#### <a href="https://losa.fr/research/assignment/">losa_ap</a>
- Specification's authors: Giuliano Losa
- Original paper: <a href="https://dl.acm.org/citation.cfm?id=3154303">Carole Delporte-Gallet, Hugues Fauconnier, Eli Gafni, and Giuliano Losa. 2018. The Assignment Problem. In Proceedings of the 19th International Conference on Distributed Computing and Networking (ICDCN '18). ACM, New York, NY, USA, Article 14, 9 pages.</a>
- Extended modules: FinSet, Nat, Seq
Expand Down
2 changes: 1 addition & 1 deletion specifications/losa_rda/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### losa_rda
#### <a href="https://www.losa.fr/Thesis.pdf">losa_rda</a>
- Specification's authors: Giuliano Losa
- Original paper: <a href="https://www.losa.fr/Thesis.pdf">Losa, Giuliano. Modularity in the design of robust distributed algorithms. Diss. Ph. D. thesis, Ecole Polytechnique Federale de Lausanne, 2014.</a>
- Extended modules: FinSet, Nat, Seq
Expand Down
2 changes: 1 addition & 1 deletion specifications/m2paxos/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### m2paxos
#### <a href="https://github.com/visualzhou/mongo-repl-tla">mongo-repl-tla</a>
- Specification's authors: Giuliano Losa
- Original paper: <a href="https://ieeexplore.ieee.org/document/7579738/">Peluso, Sebastiano, et al. Making fast consensus generally faster. Dependable Systems and Networks (DSN), 2016 46th Annual IEEE/IFIP International Conference on. IEEE, 2016.</a>
- Extended modules: Int, Seq, FinSet
Expand Down
2 changes: 1 addition & 1 deletion specifications/mongo-repl-tla/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### mongo-repl-tla
#### <a href="https://github.com/visualzhou/mongo-repl-tla">mongo-repl-tla</a>
- Specification's authors: Siyuan Zhou
- Original paper: <a href="https://raft.github.io/raft.pdf">Ongaro, Diego, and John K. Ousterhout. In search of an understandable consensus algorithm. USENIX Annual Technical Conference. 2014.</a>
- Extended modules: FinSet, Nat, Seq
Expand Down
2 changes: 1 addition & 1 deletion specifications/nfc04/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### nfc04
#### <a href="http://www.steffen-zschaler.de/publications/NfC04/">nfc04</a>
- Specification's authors: Steffen Zschaler
- Original paper: <a href="https://link.springer.com/article/10.1007/s10270-009-0115-6">Zschaler, Steffen. Formal specification of non-functional properties of component-based software systems. Software & Systems Modeling 9.2 (2010): 161-201.</a>
- Extended modules: Real, Nat
Expand Down
2 changes: 1 addition & 1 deletion specifications/raft/README.md
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
#### raft
#### <a href="https://github.com/ongardie/raft.tla">raft</a>
- Specification's authors: Diego Ongaro
- Original paper: <a href="https://raft.github.io/raft.pdf">Ongaro, Diego, and John K. Ousterhout. In search of an understandable consensus algorithm. USENIX Annual Technical Conference. 2014.</a>
- Extended modules: FinSet, Nat, Seq
Expand Down

0 comments on commit c32deaa

Please sign in to comment.