Scalable Atomic Visibility with RAMP Transactions

Scalable Atomic Visibility with RAMP Transactions - Bailis et al. 2014 RAMP transactions came up last week as part of the secret sauce in Coordination avoidance in database systems that contributed to a 25x improvement on the TPC-C benchmark. So what exactly are RAMP transactions and why might we need them? As soon as you … Continue reading Scalable Atomic Visibility with RAMP Transactions

SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems

SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems - Leesatapornwongsa et al. 2014 This is the second of three papers we'll be looking at this week on the theme of verifying correctness of, and catching bugs in, distributed systems. Yesterday we saw the Statecall Policy Language and associated tool chain … Continue reading SAMC: Semantic-aware model checking for fast discovery of deep bugs in cloud systems

Combining static model checking with dynamic enforcement using the Statecall Policy Language

Combining static model checking with dynamic enforcement using the Statecall Policy Language - Madhavapeddy 2009 We know that getting distributed systems right is hard, and subtle, 'deep' bugs can lurk in both algorithms and implementations. Can we do better than informal reasoning coupled with some unit and integration tests? Evidence suggests we have to do … Continue reading Combining static model checking with dynamic enforcement using the Statecall Policy Language