‘Experience of software engineers using TLA+, PlusCal and TLC’ [slides] [pdf]
by Chris Newcombe, an AWS principal engineer. Several Amazonians sharing their results in simulating tricky distributed-systems problems using formal methods
(tags: tla+ pluscal tlc formal-methods simulation proving aws amazon architecture design)
LinkBench: A database benchmark for the social graph
However, the gold standard for database benchmarking is to test the performance of a system on the real production workload, since synthetic benchmarks often don’t exercise systems in the same way. When making decisions about a significant component of Facebook’s infrastructure, we need to understand how a database system will really perform in Facebook’s production workload. [….] LinkBench addresses these needs by replicating the data model, graph structure, and request mix of our MySQL social graph workload.
Mentioned in a presentation from Peter Bailis, http://www.hpts.ws/papers/2013/bailis-hpts-2013.pdf(tags: graph databases mysql facebook performance testing benchmarks workloads)