Posts

Seven Reading Suggestions for the Holidays

Image
One time I asked a very experienced engineer about his favorite technical books. He told me: "I barely read technical books. I have learned what I know mostly through experience while building useful things". I totally agree; experience is very important. Nothing can replace experience; no university degree, certificate, or amount of knowledge can compensate for the lack of experience. So next time you see a job posting with 10+ years of experience requirement, don't get upset if you don’t have it, because certain things just take time.  Having said that, I think it is still a good idea to constantly read technical books/papers for several reasons. Firstly, it is fun. Personally, nothing gives me more pleasure than being exposed to new ideas and organizing my knowledge around a subject. Also, we don't want to reinvent the wheel. Every year, some of very smart people publish the results of their hard work through conferences and journals. Why ignoring them and trying t...

Amazon DynamoDB: ACID Transactions using Timestamp Ordering

Image
Amazon DynamoDB uses a lightweight transaction protocol via timestamp ordering. Although both Spanner and DynamoDB use timestamps in their transaction protocol, DynamoDB seems significantly simpler than Spanner; while Spanner uses 2PL and MVCC and needs TrueTime, DynamoDB only relies on timestamp ordering and does not use any locking or MVCC scheme. In this post, we want to review the DynamoDB transaction protocol and compare it with Google Spanner. 

Exactly-Once Delivery

Image
Exactly-Once Delivery (EOD) is a very useful guarantee to have when designing a distributed system; being sure that no message is lost or delivered more than one time, despite all possible faults, makes the design of any distributed systems simpler. Intuitively, EOD is clear: we don’t want to lose or duplicate the data/operations. The exact definition, however, is not agreed upon in the community. As a result, there is a debate on whether EOD is possible or impossible to achieve. In this post, we focus on EOD, its possibility/impossibility, and what it really means in practice.  

Graph Databases

Image
Graph data is very common in modern applications. The property of this kind of data is the high levels of connectivity between the entities. Although social networks are the most common example for demonstrating graph data and the importance of graph databases, graphs are not limited to social networks; many other applications can be modeled much more clearly and intuitively with graphs. Once we model our data as a graph, we usually want to explore certain parts of the graph to find relations or interesting patterns. That includes simple use cases such as finding a person's friends or friend-of-friends in a social network, or complex patterns revealing frauds in a financial graph. All these applications require fast traversal of graph nodes. Although we can store a graph in a tabular relational database or a NoSQL database such as key-value/document stores, they typically don't provide fast traversal which is critical for graph applications. In this p...

Practical Tips on using TLA+ and P

Image
TLA+ and P are formal specification languages that let us formally define the behavior of our system and have a model checker reason about its correctness. In this post, I want to share some practical tips on using these awesome tools. I am not going to explain the basics and I assumes the reader is already familiar with these languages. If you are not, you can learn more about TLA+ at  Leslie Lamport's website . For P, a great place to start is the official website . I also wrote a blog post on P that explains P with examples. TLA+ vs. P While both TLA+ and P are formal specification languages, they are used for different purposes. Proving vs. Testing The main difference between TLA+ and P is that TLA+ is used to  prove , while P is used to  test ,   the correctness. While both use model checking, only TLA+ is used for exhaustive model-checking where we explore all possible executions of a given specification. Thus,  when the model checker does not find a bug,...

Model-based Testing Distributed Systems with P Language

Image
P is the name of a domain-specific language for asynchronous event-driven programming. With P, we can specify a system as a set of interacting state machines which talk to each other by sending events. That makes P a suitable language for modeling distributed systems where nodes talk to each other asynchronously via messages. P originally developed by Microsoft and according to its Github repository, it is currently being used extensively inside Amazon AWS for model-checking complex distributed systems. In this post, we want to see how we can use P to catch bugs in our protocols. 

State Machine Replication with Raft

Image
In this post, we want to review the Raft algorithm which is a leader-based consensus algorithm. Raft is a simpler and more understandable alternative to Multi-Paxos, and since its relatively recent invention, it has been widely adopted in the industry. Unlike Multi-Paxos that extends an algorithm that is originally designed for consensus on a single value, Raft directly considers the problem of consensus on a sequence of values. This makes Raft much more practical and understandable than Multi-Paxos.