Aug 19, 2016 - Disciplined Inconsistency

Today, in our reading group, we read an interesting paper titled “Disciplined Inconsistency” by Brandon Holt et al from UW CSE. This post is my notes on the paper.


Modern day web-services often trade consistency for availability and performance. However, there exist some data and operations for which stronger forms of consistency are needed. Recognizing this, some data stores, including Quelea, implement stronger consistency guarantees, such as Causal Consistency. However, there are two major problems with the lattice-of-consistency-levels model espoused by Quelea:

  • In real applications, invariants over the data are almost never strict. Applications can tolerate certain amount of error, especially if it improves the performance. For example, Amazon can afford to oversell a discounted item by 2% of the available stock, but no more. Unfortunately, Quelea’s model is insensitive to such error bounds. Quelea expects applications to have exact invariants, such as non-negative balance or monotonicity, and attempts to statically determine appropriate consistency levels that can enforce these invariants without fail. In reality, applications execute under moderate-to-medium loads during most of their lifetimes, under which weaker consistency levels are more-or-less sufficient to maintain application invariants. Quelea’s consistency model lacks dynamic monitoring, thus cannot adapt consistency to the changing load conditions.
  • The flow of data between operations executing at various consistency levels is not controlled. Consequently, data being maintained at EC can make its way into the data being maintained at SC.

Holt et al propose a system called IPA (Inconsistent, Performance-bound, Approximate storage system) that addresses the above problems via a combination of static type system and runtime enforcement. In the following, I explain various aspects of IPA in greater detail.

IPA’s Programming Model

IPA is modeled as a data structure store, like Redis, Riak, and Hyperdex, and its Scala-based programming framework allows programmers to implement ADTs, such as sets and counters, as distributed data structures. To better understand IPA’s approach, let us distinguish between library writers, who implement ADTs, and app developers, who use ADTs. IPA expects library writers to define various versions of an ADT, each with a different combination of consistency policies for ADT operations. In Scala’s terminology, each combination is a trait of the ADT. For instance, Counter ADT can be defined with, say, two traits: a WeakOps trait that implements counter reads and increments using Cassandra’s weak (i.e., consistency level ONE) reads and writes, and a StrongOps trait that implements them via Cassandra’s QUORUM reads and writes, or via ONE writes and ALL reads. For more sophisticated ADTs, more combinations of consistency levels for operations can be implemented as traits. App developers use the ADTs defined by library writers by selecting a version with desired trait. For instance, an app developer may use the Counter ADT with StrongOps trait to obtain a strongly consistent counter, or with WeakOps to obtain a weakly consistent counter.

From IPA’s perspective, Strong and Weak are examples of static consistency policies. IPA also provides support for library writers to implement traits for dynamic consistency policies, such as LatencyBound and ErrorBound, which admit bounds on the latency of an operation and the error tolerance on its result (resp.). For instance, LatencyBound trait for Counter ADT can be implemented using the rush primitive offered by IPA that executes a read or a write under strongest consistency level possible within the specified time limit. Likewise, ErrorBound trait can be implemented via IPA’s support for escrow reservations. Both these mechanisms will be explained in detail later. An app developer, however, does not need to know about these implementation mechanisms. The developer can choose Counter with LatencyBound(50) trait to obtain a counter whose operations have a 50ms latency bound, or Counter with ErrorBound(10) trait to obtain a counter whose value can be off by at most 10% of the actual count.

IPA thus exposes different levels of abstractions to library writers and app developers. While app developers can think in terms of ADTs and high-level consistency policies, library writers have to face the ugliness of the underlying data store as they reason in terms of reads, writes, and low-level consistency policies, such as ONE, QUORUM etc. While IPA does provide some tool support (via rush and reservations), it does not raise the level of abstraction insofar as library writers are concerned. This is in contrast to Quelea where RDT writers also reason in terms of high-level consistency policies and RDT-specific effects.

Static Type System

The stated purpose of IPA’s consistency type system is to enforce consistency safety Informally, it “ensures that values from weakly consistent operations cannot flow into stronger consistency operations without explicit endorsement form the programmer”. Thus, the type system helps developers trade consistency for performance in a disciplined manner.

IPA’s implementation defines four consistency types:

  • Consistent[T]: A value of type T resulting from a strongly consistent operation (the StrongOps trait),
  • Inconsistent[T]: A value of type T resulting from a weakly consistent operation (the WeakOps trait),
  • Rushed[T]: A value of type T resulting from an operation executed with a latency bound (the LatencyBound trait), and
  • Interval[T]: A range of values of type T, each of which is equally likely to be the result of an operation executed with an error bound (the ErrorBound trait).

The return type of an ADT operation is either defined by the library writer while implementing the trait, or follows from the use of IPA primitives, such as rush. Thus, more consistency types can be defined by library writers. For example, consider a Facebook-like deployment where an object is only ever stored in a single data center. If an ADT is tailor-made for such deployment, its writer can implement its operations via LOCAL_QUORUM reads and writes, and claim per-object sequential consistency by annotating the return types of operations with a new Consistent[PoSC] type.

A subtype lattice over consistency types can also be defined by relying on Scala’s type system. For instance, here is a lattice defined by the IPA implementation, and presented in the paper:


The result of annotating return values with consistent types is that app developers must now explicitly handle non-Consistent[T] values:

  • If a value is Inconsistent[T], the developer must explicitly endorse the value for it to be treated on par with Consistent[T] values.
  • If it is Interval[T], the result of an ErrorBound operation, then the developer has to handle an interval of values.
  • Rushed[T] is implemented as “a sum type with one variant per consistency level available to the implementation of LatencyBound” (It’s not quite clear to me how this is done). Thus, a Rushed[T] value has to be destructed and matched against Consistent[T], or Inconsistent[T], or any other user-defined (static) consistency type before it is used.

Thus consistency types let application be sensitive to the consistency level of a value. Alternatively, they force the application to adopt a disciplined approach while dealing with inconsistent values.

Run-time enforcement of consistency

Strong consistency is implemented using QUORUM reads and writes. As we describe in Representation without Taxation paper, such an implementation is likely to be buggy since Cassandra’s LWW conflict resolution drops writes due to inevitable clock drift across servers.

LatencyBound reads are implemented in IPA by issuing parallel read requests at different (Cassandra) consistency levels, and returning the strongest available result at the specified time limit. One drawback with this approach is that it floods network with read requests, which is undesirable esp. when system is operating at high loads. Therefore, the paper proposes an alternative approach that is based on monitoring latency. The approach first computes the likely latency (e.g., 90th percentile latency) of a read operation for each consistency level based on the recent history, and then issues the read at an appropriate level. For this purpose, the system monitors latencies of reads, grouped by operation and consistency level. “The monitor uses an exponentially decaying reservoir to compute running percentiles weighted toward recent measurements, ensuring that its predictions continually adjust to current conditions”.

IPA allows ADTs to implement error bounds making use escrow and reservation. The paper summarizes this concept well:

The idea is to set aside a pool of permissions to perform certain update operations (we’ll call them reservations or tokens), essentially treating operations as a manageable resource. If we have a counter that should never go below zero, there could be a number of decrement tokens equal to the current value of the counter. When a client wishes to decrement, it must first acquire sufficient tokens before performing the update operation, whereas increments produce new tokens. The insight is that the coordination needed to ensure that there are never too many tokens can be done off the critical path: tokens can be produced lazily if there are enough around already, and most importantly for this work, they can be distributed among replicas. This means that replicas can perform some update operations safely without coordinating with any other replicas.

Consider an increment-only counter X. Let us say X = 100 initially, and the error bound on X is 10%. Consider a case when 3 replicas are independently modifying X. Then, replicas can be issued 5 tokens each, capturing the fact that each can perform 5 increments before they need to synchronize in order to not violate error bounds. For instance, if all replicas perform 5 increments each without synchronizing, then each will return 105 as the value of X when the actual value is 115. However, 105 is still within 10% of 115, so this is alright. Thus, error bounds provide applications with some slack in implementing strongly consistent operations by allowing synchronization to be moved off the critical path.

IPA provides infrastructure support (via reservations server) for escrow reservations, and exposes its functionality via an API. The library writer is expected to make use of this functionality to implement ErrorBound consistency policy for his/her ADT.

An Aside

The escrow method was proposed in 1986 (and rehashed later), but there seem to be many recent papers on applying variants of escrow in various contexts:

  • Liu et al, Warranties for Faster Strong Consistency, NSDI’14 (paper).
  • Balegas et al, Putting Consistency Back into Eventual Consistency, EuroSys’15 (paper)
  • Balegas et al, Extending Eventually Consistent Cloud Databases for Enforcing Numeric Invariants, SRDS’15 (paper)

I have the intuition that escrow methods would be useful to implement merge operation on data structures that support non-commutative and non-idempotent operations. Basically, if we allocate n tokens to each replica to perform a non-idempotent operation, such as a dequeue operation on a queue, n times (where n is the size of the queue), then merge operation becomes simple because a dequeue only dequeues an item present on all replicas. We also get the read at least once guarantee on the messages in the queue.


The experimental methodology of the paper is interesting, and results are insightful. Experiments are performed for two different setups: simulation and real. In simulation experiments, they use multiple docker containers on the same physical node connected via the Ethernet to simulate multiple replicas. Network conditions are controlled via Linux’s tc netmem utility that introduces packet delay and loss at the OS level. In real experiments, they deploy IPA on Google’s Compute Engine with geo-distributed replicas.

Three kinds of experiments were performed: 1. With uniform 5ms network latency between replicas (simulating a local network in a data center under medium-to-high load), 2. With one replica being slower than other replicas (modeling variable network latency and hardware problems), and 3. With real geo-distributed replicas. Some highlights:

  • In experiments with a single slow replica, 50ms bound on the 95th percentile latency overloads the slow replica with double the requests (why?), and causes it to exceed the latency bound 5% of times.
  • In geo-distributed case, if all operations are SC, then the mean latency is 800ms, but if 1% error is tolerated (on the Counter), then the latency reduces significantly to 200ms. The latency difference between weak consistency policy and 5% ErrorBound consistency policy is negligible. This experiment demonstrates that it is possible to guarantee error bounds on the data without having to forego availability and performance.
Continue reading

May 31, 2016 - Extraction in Coq

Extraction erases Props

Extraction in Coq works by erasing Props. For example, consider the following definition of div:

    Definition div (m n : nat)(H : n<>0): nat :=
      NPeano.div m n.

div expects a proof that its second argument is non-zero. Indeed, in coq, it is impossible for div to divide by zero. However, when this code is extracted to OCaml, the n <>0 prop is erased (Coq renames our div to div0 to avoid name clash with NPeano’s div):

let div0 m n = div m n


Coq’s sumbool type is another good example to demonstrate the proof erasing nature of extraction. sumbool is defined in Specif module as following:

(** [sumbool] is a boolean type equipped with the justification of
    their value *)

Inductive sumbool (A B:Prop) : Set :=
  | left : A -> {A} + {B}
  | right : B -> {A} + {B}
 where "{ A } + { B }" := (sumbool A B) : type_scope.

sumbool is usually the return type of equality decision procedures of various types. For example, the string_dec, the string equality function has the type:

  forall s1 s2 : string, {s1 = s2} + {s1 <> s2}

Consider a type id defined as:

  Inductive id : Type :=
    T : string -> t.

A decision procedure ids can be constructed from string_dec as following:

 Theorem eq_id_dec : forall id1 id2 : id, {id1 = id2} + {id1 <> id2}.
     intros id1 id2.
     destruct id1 as [n1]. destruct id2 as [n2].
     destruct (string_dec n1 n2) as [Heq | Hneq].
     Case "n1 = n2".
       left. rewrite Heq. reflexivity.
     Case "n1 <> n2".
       right. intros contra. inversion contra. apply Hneq. apply H0.

Extracting the sumbool and eq_id_dec generates the following:

      type sumbool =
      | Left
      | Right
      (** val eq_id_dec : t -> t -> sumbool **
      let eq_id_dec id1 id2 =
        string_dec id1 id2

OCaml’s sumbool has no arguments because coq’s sumbool has only Prop arguments. The advantage of using sumbool instead of bool is that it can be used seamlessly in proofs and computations. When used in a computation, sumbool simply tells whether a property is true or false, but when used in a proof, sumbool also tells why a property is true or false.

Theorems can also be extracted

Observe that eq_id_dec has been written as a theorem. Theorem can be used to assert the existence of a witness to, not only Props, but also Sets and Types. For example:

  Theorem there_is_a_nat : nat.
  Proof.  apply 0.  Defined.

  Extraction there_is_a_nat.
    let there_is_a_nat = O

Why do we say Defined instead of Qed whenever we are doing extraction? Qed defines proof/definition as opaque, whereas Defined defines it as transparent. If we used Qed instead of Defined extraction would produce:

(** val there_is_a_nat : nat **)

let there_is_a_nat =

Note that theorems can only be extracted if the statement is either Set or a Type, not Prop. The following two examples should demonstrate this point. Example 1:

  Theorem there_is_plus: forall (n1 n2 : nat), exists (n :nat), n = n1 + n2.
  Proof.  intros.  exists (n1+n2).  reflexivity.

  Check (forall (n1 n2 : nat), exists (n :nat), n = n1 + n2). (* Prop *)

  Extraction there_is_plus.
      (** val there_is_plus : __ **)

      let there_is_plus =

Contrast Example 1 with the following Example 2:

  Inductive plus_defined (n1 n2: nat) : Set :=
    | PlusT : forall(n:nat), (n=n1+n2) -> plus_defined n1 n2.

  Extraction plus_defined.
      type plus_defined =
        nat (* singleton inductive, whose constructor was PlusT *)

  Theorem there_is_plus_t: forall (n1 n2 : nat), plus_defined n1 n2.
  Proof.  intros.
  apply PlusT with (n:=n1+n2); reflexivity.

  Extraction there_is_plus_t.
    let there_is_plus_t n1 n2 = plus n1 n2

Why would anyone want to write a Set or a Type term as a proof of a theorem, rather than a Definition or a Fixpoint? If the Set or Type term expects Prop witnesses (like sumbool), then its better to write it as a proof. Sometimes, it may not even be possible to write the term otherwise. For example, here is a failed attempt at defining eq_id_dec as a Definition:

  Inductive id : Type :=
    T : string -> t.

  Theorem eq1 : forall (s1 s2: string), s1=s2 -> (T s1) = (T s2).
    subst. reflexivity.

  Theorem neq1 : forall (s1 s2 : string), s1<>s2 -> (T s1) <> (T s2).
  unfold not.
  apply H; inversion H0. subst; reflexivity.

  Definition id_eq (id1 id2 : id) : ({id1 = id2}+{id1 <> id2}) :=
    match (id1,id2) with
    | (T s1,T s2) => match string_dec s1 s2 with
                     | left A => left (eq1 s1 s2 A)
                     | right B => right (neq1 s1 s2 B)

The approach fails because the term left (eq1 s1 s2 A), which has the type {T s1 = T s2} + {?66}, fails to type check agains the required type {id1 = id2} + {id1 <> id2}. The problem is that while pattern matching under a definition, coq does not populate the context with equalities between scrutinees and patterns. Although we know that id1 = T s1 and id2 = T s2, we have no way of obtaining it from the context. Recall that we did not face this problem when proving eq_id_dec. This is why we sometimes prefer writing Set or Type terms as proofs.

Continue reading

Dec 5, 2015 - Notes - Terry's Session Guarantees


This post is the compilaton of my notes on Terry et al’s PDIS’94 paper: Session Guarantees for Weakly Consistent Replicated Data.

System Model

From what I understand, the paper is the first to describe the abstract system model of a weakly consistent replicated database that now serves as a frame of reference to describe KV stores (eg., Cassandra and Riak) and mobile computational nodes. The abstract system model is very similar to Quelea’s system model described in Sec.2 of the PLDI paper. Like in Quelea, where the state of an application at a replica \(r\) is the set of application-specific effects present at that replica (i.e., \({\sf vis}\) set at \(r\)), the application state at server \(S\) in Terry’s model the collection of app-specific Write’s at \(S\) (denoted \(DB(S)\)). Following is a more detailed comparison:

  • A Write in Terry’s model is an abstraction of creation, updatation, or deletion of concrete data items (collectively called CUD operations). Hence, multiple Write operations need not commute. The \({\sf WriteOrder}\) therefore assumes significance. A Write in Quelea is an abstraction of a single atomic effect. Quelea’s model in general encourages commutative Writes, and the model does not have a built-in notion of a \({\sf WriteOrder}\). Application state in Quelea is a set of effects, and the result of a Read operation is obtained by folding over this set. Nonetheless, Quelea model does not preempt CUD operations; it is possible to write applications with Read, Write and Delete operations, such as registers, in Quelea. However, applications have to implement their own mechanisms (eg., tagging effects with local timestamps) and conflict resolution semantics (eg., Last-Writer-Wins) to ensure convergence.
  • Both models rely on total propagation and consistent ordering to ensure eventual consistency. Total propagation can be achieved via anti-entropy mechanisms such as hinted-handoff and read-repair (more about these in this paper). In Quelea’s implementation, this is taken care by Cassandra. No further assumptions about total propagation are made. Consistent ordering for non-commutative writes is essential for convergence. Both models rely on application semantics to consistently order writes at all replicas. However, while Terry’s abstract model takes cognisance of the write order via the binary \({\sf WriteOrder}\) predicate, Quelea’s model (intriguingly) does not.
  • A Write in Terry’s model is an abstraction of multiple CUD operations, which appear to take place atomically. Hence, Terry’s Writes are in fact transactions with RC isolation level.

Session Guarantees

In Terry’s and Quelea’s perspective, a session is an abstraction of a sequence of Read and Write operations performed during the execution of an application. Note that operations from the same client session can be dispatched to different replicas, hence the result of a read operation in a session may not be consistent with the write operations performed previously in the same session. This could be very annoying to the end user. The purpose of the paper is to equip the aforedescribed abstract system model with additional guarantees that collectively ensure that the results of operations performed in a session will be consistent with the model of a single centralized server, possibly being read and updated concurrently by multiple clients.

Terry et al propose four session guarantees for their model, and, due to the close correspondence between both models, they can also be (nearly) stated as specifications in Quelea’s spec language. Below, I present both versions (Note: what Terry calls \({\sf RelevantWrites}\), Quelea calls\({\sf Visibility}\)):

  • Read Your Writes: If Read \(R\) follows Write \(W\) in a session and \(R\) is performed at server \(S\) at time \(t\), then \(W\) is included in \(DB(S,t)\).
    • \(\forall a,b.\, {\sf soo}(a,b) \Rightarrow {\sf vis}(a,b)\)
  • Monotonic Reads: If Read \(R_1\) occurs before \(R_2\) in a session and \(R_1\) accesses server \(S_1\) at time \(t_1\) and \(R_2\) accesses server \(S_2\) at time \(t_2\), then \({\sf RelevantWrites(S_1,t_1,R_1)}\) is a subset of \(DB_{}(S_2,t_2)\).
    • \(\forall a,b,c.\, {\sf vis}(a,b) ~\wedge~ {\sf soo}(b,c) \Rightarrow {\sf vis}(a,b)\)
  • Writes Follow Reads: If Read \(R_1\) precedes Write \(W_2\) in a session and \(R_1\) is performed at server \(S_1\) at time \(t_1\), then, for any server \(S_2\), if \(W_2\) is in \(DB(S_2)\) then any \(W_1\) in \({\sf RelevantWrites}(S_1,t_1,R_1)\) is also in \(DB(S_2)\) and \({\sf WriteOrder_{}}(W_1,W_2)\).
    • \(\forall a,b,c,d.\, {\sf vis}(a,b) ~\wedge~ {\sf soo}(b,c) ~\wedge~ {\sf vis}(c,d) \Rightarrow {\sf vis}(a,d) ~\wedge~ ?{\sf WriteOrder}(a,c) \).
  • Monotonic Writes: If Write \(W_1\) precedes Write \(W_2\) in a session, then, for any server \(S_2\), if \(W_2\) in \(DB(S_2)\) then \(W_1\) is also in \(DB(S_2)\) and \({\sf WriteOrder_{}}(W_1,W_2)\).
    • \(\forall a,b,c.\, {\sf soo}(a,b) ~\wedge~ {\sf vis}(b,c) \Rightarrow {\sf vis}(a,c) ~\wedge~ ?{\sf WriteOrder}(a,b)\).

Observe that Terry’s \({\sf WriteOrder}\) becomes \(?{\sf WriteOrder}\) in Quelea. The punctuation is to explicitly denote the fact that Quelea is unaware of \({\sf WriteOrder}\). To make the matters worse, Quelea does not expose \({\sf happens-before}\) order to application semantics. Consequently, a straightforward port of a Bayou (Terry’s system) application, which requires WFR or MW session guarantee, onto Quelea does not preserve application semantics.

Example Alice tweets “The chicken laid an egg”. Bob sees Alice’s tweet and tweets “A chicken hatched out of the egg”. If GetTweets is tagged with WFR spec in Quelea, then Cheryl, who sees Bob’s tweet is also guaranteed to see Alice’s tweet. However, she canot figure out the causal order among the tweets making her wonder what comes first: Alice’s chicken, or Bob’s egg.

How do we overcome the handicap described above? Some thoughts:

  1. The state of an application that admits non-commutative operations is not an unordered set of effects, but a partially-ordered set of effects with respect to the \({\sf happens-before}\) relation. Accordingly, Read operations in Quelea must reduce over a graph representing the poset, but not a list representing a set.
  2. Is there a way to explicitly track causality by tagging effects with vector clocks? Since each component of the vector must represent the monotonically increasing clock local to a replica, and there is no way to know the currentReplicaId in Quelea, this approach seems implausible. However, getCurrentReplicaId is a simple extension to Quelea, hence supporting this approach is easy. Unfortunately, explicitly tracking vector clocks is tedious and complicates application logic. Hence, first approach may be preferable.
Continue reading

Oct 5, 2015 - Effing Package Management (FPM)

If you are ever into making debian packages to distribute your software, check out this great package management tool called fpm by @jordansissel. FPM is no-nonsense package manager that lets you create packages by simply specifying dependencies, and source and destination paths for your binaries, libraries and includes.


Let us say you want to make a debian package to distribute the first version of your hello-dev application, that provides a binary (hello), a dynamic library ( and an include file (hello.h), which you want to be installed in the usual locations under /usr. Also, let’s assume that your application requires gcc version 4.6.3 or above. Creating a debian package for your is as easy as:

 fpm -s dir -t deb -n "hello-dev" -v 1.0 --description "Hello development tools" -d 'gcc > 4.6.3' ./hello=/usr/bin/hello ./ ./hello.h=/usr/include/hello.h ./LICENSE=/usr/share/doc/hello-dev/copyright
Continue reading

Sep 30, 2015 - Understanding Transactions in Rails

In my previous post I have noted that Rails encourages application developers to rely on feral mechanisms, such as validations and associations, to ensure application integrity. In this post, I first explore various feral mechanisms in Rails, and how they are being used by some sample applications. Next, I will throw some light on how Rails actually enforces these feral mechanisms.

ORM and Active Record

Quoting from Ruby on Rails guide:

Object Relational Mapping: Object-Relational Mapping, commonly referred to as its abbreviation ORM, is a technique that connects the rich objects of an application to tables in a relational database management system. Using ORM, the properties and relationships of the objects in an application can be easily stored and retrieved from a database without writing SQL statements directly and with less overall database access code.

Active Record as an ORM Framework: ActiveRecord is Rails’s implementation of ORM. Active Record gives us several mechanisms, the most important being the ability to:

  • Represent models and their data.
  • Represent associations between these models.
  • Represent inheritance hierarchies through related models.
  • Validate models before they get persisted to the database.
  • Perform database operations in an object-oriented fashion.

Active Record Models: A class that extends ActiveRecord is an Active Record model, or simply a model. Each model has a corresponding table in the underlying database. For instance, defining the Product model:

class Product < ActiveRecord::Base 

will create a table with the following schema:

CREATE TABLE products (
  id int(11) NOT NULL auto_increment,
  name varchar(255),

CRUD: To write a record to the the database, we first create an Active Record object (note: arg: denotes an argument named arg. Think of Ruby methods as functions accepting named variants):

product = Product.create(name: "Milk")


product = do |p| = "Milk"

To save, ActiveRecord offers save method:

Reading can be done via multiple querying methods. Example:

all_prods = Product.all
milk = Product.find_by(name: "Milk").order(id: :asc)

Active record querying webpage has more details.

Updatation can be done via read-modify-save sequence:

milks = Product.find_by(name: "Milk")
milks.each do |m| = "Whole Milk"

Note: Active Record uses SQL INSERT for new record saves, and SQL UPDATE for updatations. It uses new_record? flag to keep track of new Active Record objects that are not yet saved into the database (source: Active Record Callbacks guide).

Deletion is done using destroy:

milks = Product.find_by(name: "Milk")
milks.each do |m| 

The corresponding records will be deleted from the database.


Associations are useful to keep track of semantic associations between various models. For instance, using a belongs_to association, the developer can let Rails know that every order in an eCommerce application belongs to utmost one customer (Note: the :name syntax denotes a symbol called name. Meta-level functions accept symbols and generate new code, which would then be spliced into original code (somewhat like MetaOCaml and TemplateHaskell). Ruby, being a dynamic language, does not treat meta-level functions specially.).

class Order < ActiveRecord::Base
  belongs_to :customer

The result is that the order table will now have a column named customer_id that is expected to refer to id of the customer table. Order objects will also have a field named customer referring to the Customer object to which the order belongs to (note: the field can be nil). When an order object is saved, the id of its customer object will be saved to the customer_id field of the corresponding record in the database.

The other end of belongs_to association is usually a has_many association or has_one association. Using a has_many association, the developer can specify that a customer can have one or many orders:

class Customer < ActiveRecord::Base
  has_many :orders

Other than adding a field named orders to a customer object, specifying the has_many association will have no tangible effect; there is no change in Rails’s interaction with order and customer tables. However, we can qualify the has_many association with an optional dependent argument set to :destroy that asks Rails to destroy all orders placed by a customer, when the customer is deleted.

class Customer < ActiveRecord::Base
  has_many :orders, dependent: :destroy

This behaviour corresponds to ON DELETE CASCADE behaviour offered by SQL for foreign key dependents.

With belongs_to association from Order to Customer, and has_many association from Customer to Order, with a dependent: :delete qualification, we have something close to, but not exactly, a foreign key constraint from the order table to the customer table. To effectively enforce a foreign key constraint, we need a guarantee that an order cannot exist without the corresponding customer existing in the customer table. Currently, this invariant can be violated if, for example, we save an order object referring to a customer object, whose corresponding record was already destroyed. The effective foreign key enforcement that prevents this scenario (theoretically, at least) can be achieved using Model Validations, described in the next section.

It is also possible to specify many-to-many relationships between models in a similar way to how such relationships are defined in relational databases: via an intermediary model. For example, in a microblogging application, a user can follow many users, and can have many users as followers. This many-to-many relationship between users can be specified via a third model called, say, relationships. Each user has_many following relationships and follower relationships. Each relationship belongs_to two users: user who is being followed, and the user who is following. This scenario is described in the picture below (source: Michael Hartl’s book. Released under MIT License):


Observe that there is a transitive has_many relationship between users, which can be made explicit via through: argument to has_many association: a user has_many followers through: relationships, and has_many followed_users through: relationships.

Besides belongs_to, has_many, and has_one, Rails defines few other associations. They are described here.


Quoting from Rails guide on validations: Validations are used to ensure that only valid data is saved into your database. For example, it may be important to your application to ensure that every user provides a valid email address and mailing address. Model-level validations are the best way to ensure that only valid data is saved into your database.

Validations are primarily declared using validates method. For example, to ensure that user provides an email address during during a new account creation (i.e., email field is not nil), and to ensure that there are no existing accounts associated with this email, we can perform presence and uniqueness validations, respectively.

class Account < ActiveRecord::Base
  validates :email, uniqueness: true, presence: true

Rails also provides variants of validates specialized for common validations:

class Account < ActiveRecord::Base
  validates_presence_of :email
  validates_uniqueness_of :email 

validates_uniqueness_of is clearly useful to ensure primary key property. Besides being useful to preempt nil values, validates_presence_of is also useful to enforce foreign key constraints, when used in conjunction with associations. For instance, in the eCommerce example, the foreign key constraint from Order to Customer can be enforced by validating the presence of customer field.

class Order < ActiveRecord::Base
  belongs_to :customer
  validates_presence_of :customer
class Customer < ActiveRecord::Base
  has_many :orders, dependent: :destroy

Another useful validation is validates_associated. You should use this helper when your model has associations with other models and they also need to be validated. When you try to save your object, valid? will be called upon each one of the associated objects. For instance, when the Customer class validates associated orders:

class Customer < ActiveRecord::Base
  has_many :orders, dependent: :destroy
  validates_associated :orders

All the orders associated with the customer are validated when the customer object is being save‘d (in this case, this entails a validation for the presence of the customer object owning orders, which is trivially true).

validates_associated works with all of the association types. Although it is by default turned off for most associations, it is by default on for has_many association. So, for the above example we needn’t explicitly specify validates_associated.

Note: Ruby has a concept of virtual attributes, which, in the context of ActiveRecord are attributes that do not get recorded in the database. Validations can also be defined over virtual attributes.

Custom validations

Validations, such as validates_presence_of, are built into Rails. Sometimes, built-in validations are not sufficient. Rails allows developers to define custom validations for this purpose. Custom validations can be defined as methods, which are used once locally, or they can be defined by implementing Rails’s ActiveModel::Validator interface. Examples of custom validators include Spree’s AvailabilityValidator, which checks whether an eCommerce inventory as sufficient stock available to fulfill an order. More on custom validations here.

When are validations enforced?

When an Active Record object is being persisted to the database (save), although this is not entirely accurate:

Validations are typically run before these commands (INSERT/UPDATE) are sent to the database. If any validations fail, the object will be marked as invalid and Active Record will not perform the INSERT or UPDATE operation. This helps to avoid storing an invalid object in the database. You can choose to have specific validations run when an object is created, saved, or updated.

There are many ways to change the state of an object in the database. Some methods will trigger validations, but some will not. This means that it’s possible to save an object in the database in an invalid state if you aren’t careful. - ActiveRecord validations callbacks guide

Validations and any callbacks registered on the state changes of the model object are queued for execution. This queue will include all your model’s validations, the registered callbacks, and the database operation to be executed. The whole callback chain is wrapped in a transaction. If any validation/callback method returns false or raises an exception the execution chain gets halted and a ROLLBACK is issued (source).

Sample Applications

We will now examine some sample applications to understand how validations and associations are being used.


First is based on a small microblogging application from the Ruby on Rails tutorial by Michael Hartl.

The app defines 3 models - micropost, user, and relationship with following associations and validations:

  • Micropost belongs_to a user, and validates user’s presence.
  • A user has an email address; validates its presence and uniqueness.
  • A user has_many follower relationships, and through: those relationships, has_many followers. Follower relationships need to be destroyed if this user is deleted.
  • A user has_many following relationships, and through: those relationships, has_many followed users. Following relationships need to be destroyed if this user is deleted.
  • A relationship jointly belongs_to a follower user and a followed user, and validates their presence.

Following are some interesting operations that the app defines:

Adding a User: Adds a user after validating that the email is present and unique.

addUser(u) = transaction do
  assert( != nil);
  dups := SQL "SELECT * FROM users WHERE email = `` LIMIT 1"
  assert (dups == []);
  SQL "INSERT INTO users VALUES (`freshId()`,``,``)";
  followUser(thisUser, thisUser); /* One must follow oneself */

Follow a User: Makes the current user follow another user.

followUser(thisUser,thatUser) = transaction do
  usr1 := SQL "SELECT * FROM users WHERE id = `` LIMIT 1";
  assert (usr1 != []);
  usr2 := SQL "SELECT * FROM users WHERE id = `` LIMIT 1";
  assert (usr2 != []);
  SQL "INSERT INTO Relationships VALUES (``,``)";

Unfollow a User: Makes the current user unfollow other user.

unfollowUser(thisUser,thatUser) = transaction do
  SQL "DELETE FROM Relationships WHERE follower_id = ``
                                 AND followed_id = ``";

getFollowers: Returns the list of users following the current user.

/* Implementation 1 : from the original sample app */
getFollowers(thisUser) = 
  SQL "SELECT * FROM users INNER JOIN relationships ON = relationships.follower_id WHERE
      relationships.followed_id = ``"

/* Implementation 2: If the data store does not support joins
            (e.g: Cassandra) */
getFollowers(thisUser) = transaction do
  rels := SQL "SELECT * FROM relationships WHERE 
                  followed_id = ``";
  followers := [];
  rels.each |rel| do
    /* The following pattern-match must always pass because:
        1. Relationship model validates presence of follower
           before persisting.
        2. When a user is deleted, all the dependent
           relationships are deleted as well.
        3. User model validates uniqueness when persisiting. */
    [follower] = SQL "SELECT * FROM users WHERE 
                    id = `rel.follower_id`";
    followers := follower::followers;
  return followers;

getFollowedUsers: Returns the list of users that the current user is following. Implementation similar to getFollowers described above.

postBlog: Posts a microblog on behalf of the current user. Validates the presence of current user record before persisiting the microblog.

postBlog(thisUser,blog) = transaction do
  usr = SQL "SELECT * FROM users WHERE id = `` LIMIT 1"; 
  assert(usr != []);
  SQL "INSERT INTO microposts (content, user_id) 
       VALUES (`blog.content`, ``)";

getTimeLine: Get a list of microposts by a user (the call is: Micropost.includes(:user).from_users_followed_by(user)).

getTimeLine(user) = transaction do
  posts := SQL "SELECT * FROM microposts WHERE 
                  user_id = ``";
  posts.each |post| do
    post.user := (SQL "SELECT * FROM users WHERE 
                  id = post.user_id LIMIT 1").first;
  return posts;

The SQL call to users table never returns an empty collection because:

  • A micropost belongs_to a user, and checks the presence of the user before persisting, and
  • When a user is deleted, the dependent microposts are also deleted.

Therefore, .first on the collection returned by SQL is always valid.

getFeed: Get a list of microposts by users being followed by the current user.

getFeed(user) = transaction do
  followed_ids := SQL "SELECT followed_id FROM relationships
                        WHERE follower_id = ``";
  uids_of_interest := :: followed_ids ;
  posts := SQL "SELECT * FROM microposts WHERE 
                  user_id IN `uids_of_interest`";
  posts.each |post| do
    post.user := (SQL "SELECT * FROM users WHERE 
                  id = post.user_id LIMIT 1").first;
  return posts;

deleteUser: Delete the current user. It has to enforce dependent: :destroy on microposts and relationships.

deleteUser(thisUser) = transaction do
  /* First, delete all microposts by this user */
  SQL "DELETE FROM microposts WHERE user_id = ``";
  /* Next, delete all relationships on this user */
  SQL "DELETE FROM relationships WHERE 
    follower_id = `` OR
    followed_id = ``";
  /* Finally, delete the user */
  SQL "DELETE FROM users WHERE id = ``";
Continue reading

Sep 28, 2015 - Understanding Transactions in Quelea

Quelea is our eventually consistent data store with an associated programming framework intended to simplify programming under eventual consistency. In this post, I describe how various applications written in Quelea employ a combination of highly available and serializable transactions to enforce application integrity. Three applications participate in this survey:

  • BankAccount: A highly available concurrent bank account application.
  • Microblog: A twitter-like microblogging site, modeled after Twissandra. The application allows adding new users, adding and replying to tweets, following, unfollowing and blocking users, and fetching a user’s timeline, userline, followers and following.
  • Rubis: An eBay-like auction site. The application allows users to browse items, bid for items on sale, and pay for items from a wallet modeled after a bank account.

First let me define what I mean by a transaction:

What is a transaction?

For all practical purposes, a transaction can be defined as a set of operations on some data, which, when executed, appear to have been executed simultaneously. We say that the set of operations has taken effect atomically. Atomicity implies that the set of effects generated by a transaction T is visible to operations in other transaction T' in its entirety, or it is not visible at all. From the perspective of the other transaction T', an operation op' in T' either sees all the effects of a transaction T, or it sees none of them. Note that this is the requirement of Read Committed (RC) isolation level. Hence, atomicity being a defining property of a transaction means that every transaction automatically experiences RC isolation level. Note that a set of effects that offers atomicity, but with stronger isolation properties than RC is also a transaction.

Transactions are used for in various applications towards different ends. Below, I describe some of the common purposes served by transactions in some sample applications:

To perform atomic updates

Transactions are primarily used in practice when we want to perform a series of actions on the data taking it through some intermediary states, where the integrity of data may be violated. In order to not expose these intermediary states, we want to wrap these actions inside a transaction so that, for observers, it appears as if all actions have been committed atomically. Typically, these actions perform updates to multiple tables or materialized views, or multiple rows in the same table. Some usecases:

  1. BankAccount:
  2. When a user saves money, then withdraw operation on the checking account, and deposit operation on the savings account should appear to have happened atomically. Intermediary state (after withdraw, but before deposit) may violate app-specific integrity constraints (e.g: user shown incorrect total bal, or user incorrectly penalized for insufficient bal etc).
  3. Microblog (Twitter):
  4. When a user (B) unfollows another user (A), then B has to be removed from A’s follower list, and A has to be removed from B’s following list. Both updates should appear to have happened atomically. Intermediate state violates app-specific integrity constraint that follows is a symmetric relation.
  5. When a user tweets, the tweet should be added to the table of all tweets, and its Id should be added to the userline materialized view against tweeter’s userId, and timeline materialized view against the userIds of all the followers. All insertions should appear to have happened simultaneously. Intermediary states may violate (a) app-specific integrity constraints (e.g: user B sees a tweet by A in his timeline, but doesn’t find the tweet in A’s userline), and (b) referential integrity (happens if data store can reorder operations, like in the case of EC stores).
  6. When user (A) blocks user (B), then B should be forced to unfollow A (the unfollow operation needs to be performed in the same way as above). Furthermore, to prevent B from re-following A, B needs to be added to A’s Blocks list, and A needs to be added to B’s IsBlockedBy list, both in the user table itself. All changes must commit atomically.
  7. Rubis (Auction site):
  8. When a user (A) bids for an item (I), then following updates need to happen atomically:
    • The bid information needs to be added to the Bids table against a new bidId.
    • bidId needs to be added against I’s itemId in ItemBids materialized view.
    • bidId needs to be added against A’s userId in UserBids materialized view.
    • I’s maxBid needs to be updated against I’s itemId in the Item table.
      The intermediate states may violate (a) app-specific integrity constraints (e.g: bid appears as top bid on the item page, but doesn’t appear in the list of bids by the bidder), and (b) referential integrity (happens if data store can reorder operations, like in the case of EC stores).
  9. When a user cancels his bid, all the above insertions need to be deleted atomically. Intermediate states may violate referential integrity (under reordering of operations).
  10. When a user (A) offers an item (I) for auction, then I needs to be added to the Items table, and its itemId against A’s userId in the UserItems table/materialized view, simultaneously.
  11. When the auction concludes, the above insertions need to be deleted atomically. Intermediate states may violate referential integrity (under reordering of operations).

To ensure consistent reads

Atomicity only guarantees that a transaction’s effects, if visible, are visible in their entirety. It does not prevent effects from becoming visible to only a subset of operations in a different transaction. Therefore, in many cases, atomicity of a write transaction itself is not sufficient to ensure that all reads witness consistent version of data; we need certain isolation gurantees on reads. Applications use transactions to achieve isolation. Usecases:

  1. BankAccount:
  2. When a user (A) saves money (an atomic transfer from checking to savings account), and immediately checks the total balance in her accounts by issuing two getBalance operations, one on each of her accounts, she might see an inconsistent balance. This can happen if first getBalance witnesses the effects of save transaction, but second does not, or vice versa. To prevent this from happening, both getBalance operations should be wrapped inside a transactions, which needs to be executed in isolation with respect to a consisten snapshot of the database.
  3. Microblog:
  4. A read operation on user A’s followers list might tell us that user B follows A, but a read of user B’s following list might return an inconsistent result. This happens if first read witnessed the followUser transaction whereas second read did not. This situation can be prevented by wrapping both reads in a transaction and insisting that this transaction be executed in isolation with respect to a consistent version of the database.
  5. When retrieving a user(A)’s profile using username, we perform two reads - one to fetch user’s uuid from his username, and other to fetch the profile details indexed by uuid. When the user A tries to view her profile immediately after registering, the first read may succeed but second read may fail due to the absence of relevant record. This happens if the first read witnesses the effects of addUser transactions, whereas the second read does not. This situation can also be avoided by wrapping both reads in a transaction and running it under an appropriate isolation.
  6. Rubis:
  7. When displaying the list of all bids on an item, we might encounter an instance of referential integrity violation, although none actually exists in the data. This can happen if a read operation on ItemBids table reads latest version of the table, whereas the subsequent read on the Bids table reads an earlier version, which may not contain certain bids. Fix for this case is same as above.

To perform consistent (integrity-respecting) updates

Making atomic updates to the data in complete isolation can still leave the data in an invalid state. This happens when multiple such atomic updates succeed in complete isolation, but the merging resultant states results in an inconsistent state. Applications use serializable transactions to preempt the possibility of a concurrent conflicting update. Usecases:

  1. BankAccount
  2. A transfer transaction from account A to account B has to be serializable with respect to all other transfer transactions from account A to gaurantee application invariant of non-zero balance.
  3. Microblog:
  4. When deactivating the account of user (A), the userId has to be removed from the following list of all her followers, and subsequently from the user table. All operations should appear to have happened simultaneously, so they have to be wrapped in a transaction. Furthermore, to prevent violation of referential integrity, the transaction has to be serializable with respect to all addFollower transactions adding followers to A.
  5. Rubis:
  6. concludeAuction and cancelBid transactions both can independently succeed possibly resulting in a state, where a bid is simultaneously a winning bid and a canceled bid. To avoid this inconsistency, cancelBid transaction needs to be serializable with concludeAuction transaction.


  • Circular referencing.
  • Let a transaction T contain an SC operation. If a transaction T' requests RR isolation w.r.t T, then T and T' are automatically serializable.
Continue reading

Sep 24, 2015 - Notes - Feral Concurrency Control


This post is a compilation of my notes on Peter Bailis et al’s SIGMOD’15 paper: Feral Concurrency Control: An Empirical Investigation of Modern Application Integrity.


Modern relational DBMs offer a range of primitives to help the developer ensure application integrity, even under the presence of concurrency: built-in integrity constraints (e.g: UNIQUE, NOT NULL, FOREIGN KEY), triggers, stored procedures to implement application-specific integrity constraints, optimistic/pessimistic locking of rows, serializable transactions etc. However, modern web application frameworks (e.g: Ruby on Rails), which promote ORM-based programming, refrain from using most of the primitives provided by the DB layer, instead choosing to reimplement them in the application layer. Consider Ruby on Rails for instance, which is an MVC web framework. Ruby on Rails lets application developers specify their data model (M in MVC) as a set of classes that implement Rails’ native ActiveRecord class. The data model can also contain application integrity constraints in form of validations and associations. For example, presence and uniqueness are a couple of validations, and belongs_to and has_many are a couple of associations supported natively by Rails. Rails implements object-relational mapping (ORM) by automatically mapping the classes (resp. objects) that constitute the data model (resp. data) to relations (resp. tuples) in the underlying DB, provided that the application code adheres to some pre-defined naming conventions. However, validations and associations are not mapped to corresponding itegrity constraints at the DB level. For instance, uniqueness validation is not mapped to MySQL UNIQUE primitive, but instead implemented by rails by performing a SELECT query and making sure that the record being inserted is not already present (all this is done within a transaction). Likewise, instead of mapping belongs_to association to FOREIGN KEY constraint native to DB, rails implements it by running a SELECT WHERE query to check that the key being referred to is indeed present.

Eschewing native database integrity and concurrency control solutions, Rails has developed a set of primitives for handling application integrity at the application level itself, thereby building, from the perspective of the underlying DB, a feral concurrency control system. The motivation behind this apparent irrationality is to enhance maintainability of the system, and to facilitate testing. Let me elaborate:

  • Maintainability: The set of available integrity and concurreny control mechanisms at the database layer depends on the data model employed by the underlying database, and also, in some cases, on the vendor. For instance, while relational data model supports foreign key constraints as a means to implement referential integrity, data models employed by weakly consistent data stores do not. Even among relational data stores, some (e.g: PostgresSQL) support foreign key constraints, while some other (e.g: MySQL’s MyISAM and NDB storage engines) do not. Likewise, the CHECK constraint used to check domain-specific integrity constraints, such as bal ≥ 0, is supported by PostgresSQL, but not supported by MySQL. Futhermore, besides standard validations and associations, such as uniqueness and foreign key constraints, Rails allows developers to define application-specific validations and associations, for which the corresponding native primitives may not exist, and even if they exist, it is not clear how to do the mapping. To make matters worse, DB systems usually silently ignore any constraint that they do not support. Therefore, an application that relies on DB’s native constraints to enfore integrity risks correctness, is not portable, and is consequently difficult to maintain.
  • Testing: Database’s referential integrity constraints “get in the way of” testing by insisting that test data be inserted/deleted into/from the database in a specific order such that the integrity is never violated. In many cases, developers want to simply dump the sample data (known to be consistent) into the database and get along with testing their application. Requiring that such data still be inserted/deleted respecting referential integrity might be an overkill.

The aforementioned reasons, along with some personal convictions of its creators, has motivated Rails to eschew concurrency and integrity controlling mechanisms at the database layer, and view it simply as a table storage. This approach of Rails has been hugely successful, as evident from its large-scale adoption.

Replacing database native primitives with feral mechanisms may improve maintainability of the application, but does it really work? Are the feral invariants correctly enforced in Rails? Do they work in practice? This paper performs theoretical analysis and emperical studies to answer these questions.

How prevalent are feral mechanisms in practice?

They are quite prevalent. Analyzing a corpus of 67 popular opensource web applications, authors found that applications, on average, used just 3.8 transactions against 52.4 validations and 92.8 associations (median could’ve been a better metric). The overwhelming number of associations relative to transactions indicates that Rails developers use associations to perform referential integrity preserving insertions into multiple tables, which is otherwise performed in a transaction.

Rails Concurrency Control Mechanisms

Implementing validations (e.g: uniqueness) and associations (e.g: belongs_to) in the application layer is trivially safe in the sequential setting. But, in the presence of concurrent client requests attempting to modify the database simultaneosly, some concurrency control mechanisms are needed in order to ensure that validations and associations are indeed being enforced correctly. Otherwise, data integrity is jeopardized. Towards this end, Rails does the following:

  • When a model state is being updated (for e.g., during an insertion), Rails runs all the validations on the model sequentially, in a (database-backed) transaction. The rationale is to rely on ACID guarantees of the transaction to ensure the correctness of validation. For instance, uniqueness validation (by issuing a SELECT query to the database) is performed within a transaction so as to preempt concurrent insertions that may result in duplicates.
  • Associations are validated in the similar way: by enclosing the the corresponding validations inside a transaction.

If transactions are serializable as expected, then validations are indeed safe. However, databases do not offer serializable transactions by default (the default isolation level in PostgresSQL is RC. In MySQL (InnoDB), it is RR.), and, in some cases, they do not offer serializability at all. Given the possibility of concurrent transactions under weaker isolation levels (for e.g., RC ensures that visible transactions are entirely visible. It doesn’t guarantee total order among transactions.), Rails validations may not really ensure the validity of data. Examples:

  • Concurrent uniqueness validations can independently succeed, thus allowing concurrent duplicate insertions.
  • Association (e.g: foreign key) checking in one transaction, and record deletion in a concurrent transaction can independently succeed, thus compromising referential integrity.

Rails acknowledges these anomalies. The documentation warns that uniqueness validation can still occassionally admit duplicates, and association validation can occassionally result in violation of referential integrity.

How likely are these anomalies in practice?

Not very likely. For instance, in LinkBench workload capturing Facebook’s MySQL record access pattern, with 64 concurrent clients issuing 100 insert requests per second on 1000 different keys, an average of 10 duplicate records were observed when uniqueness validation is turned on. In less adversarial production workload, we may get much less number of duplicates, or maybe no duplicates. Therefore, it may be argued that validations are “good enough” for many web applications, where correctness is not a top priority.

However, concurrency is not the only reason for incorrect application behaviour. Quite often, anomalies might also result because of the incorrect implementation of a validation/association in Rails framework, or because of some non-trivial interactions between various application-level validations that Rails developers haven’t foreseen. For instance, in Rails, delete_all operation, unlike the delete operation, doesn’t create objects for rows it is deleting, thus failing to perform validations on the data being deleted (note: validations are performed only when a data model object is updated). This could result in the violation of referential integrity, resulting in http error messages being shown to user, as in the case of thoughtbot, a popular blogging platform. Thoughtbot has since started relying on PostgresSQL’s foreign key constraints to enforce referential integrity. Similar experiences have prompted few other Rails users to start a forum called Rails devs for data integrity (ref) that advocates strengthening Rails validations with database-backed checks.

What can be done about the anomalies?

Most databases natively support UNIQUE constraint, which ensures absence of duplicates at no extra expense. It is therefore a shame if one is forced to choose an incorrect implementation instead of a similar performing correct implementation just for software engineering reasons. Can something be done about this?

One solution is to insist that all validations are done inside serializable transactions (i.e., choose serializability instead of the default RC or RR isolation level at the database layer). This trivially ensures correctness of all feral implementations. Unfortunately, serializability comes at the cost of availability, which is a more important in the context of web applications. Moreover, the study finds that 75% of application invariants do not need serializability for correct enforcement. Imposing serializability by default is therefore unjustified.

The paper concludes that there is currently no database-backed solution that “respects and assists with application programmer desires for a clean, idiomatic way means of expressing correctness criteria in domain logic”. Authors believe that “there is an opportunity and pressing need to build systems that provide all three criteria: performance, correctness, and programmability.” To domesticate feral mechanisms, the authors argue, application users and framework authors need a new database interface that will enable them to:

  1. Express correctness criteria in the language of their domain model, with minimal friction, while permitting their automatic enforcement. Any solution to domestication must respect ORM application patterns and programming style, including the ability to specify invariants in each framework’s native language. An ideal solution for domestication should provide universal support to applications’ feral invariants with no additional overhead for application developers.
  2. Only pay the price of coordination when necessary. As already discussed, serializable transactions only when needed.
  3. Easily deploy the framework/application across multiple database backends. For example, the interface must allow Rails to talk to a relational store, as well as a key-value store.


“Rails can’t be trusted to maintain referential integrity, but you know what’s really good at doing that? Our relational database.” - thoughtbot

“Even when both systems are configured to one of the strict levels of transaction locking, the differences between the two implementations are subtle enough that which implementation will work better for a particular application is hard to state definitively. “- postgresql wiki.

Continue reading

Jul 31, 2015 - Atomicity vs Isolation

From the perspective of a transaction,

  • Isolation: How should I see effects of other transactions.
  • Atomicity: How other transactions see my effects.

Jul 25, 2015 - ML Type Inference

One of the most useful features of ML-family languages (OCaml, Standard ML, F# etc) is the type inference. This post contains the notes I took when I was trying to understand the foundational principles of ML type inference.

Damas-Milner Algorithm for Type Inference

Let us take a look at the original type inference algorithm produced by Damas and Milner. Their language is lambda calculus with let expression:

e ::= x | λx.e | e e | let x=e in e 

Type language composed of a set of type variables (α) and primitive types (ι).

τ = α | ι | τ → τ
σ = τ | ∀α.σ

A Type substitution is [τ1/α1, τ2/α2, ... , τn/αn]. It distinguished between an α, a type, and α, a type variable.

We define a relation (≥) that relates a more polymorphic type to a less polymorphic type. For eg, ∀α.α→α ≥ ∀β.β list → β list.

Typing judgment is Γ⊢e:σ.

Instantiation rule is also subtyping rule, where subtyping is defined in terms of “more polymorphic”:

Γ⊢e:σ₁   σ₁≥σ₂

Since there is no explicit big-lambda expression, generalization rule is important:

Γ⊢e:σ  α∈FV(σ)  α∉FV(Γ)

Basically, ∀α.σ is closure of σ w.r.t Γ (denoted \(\bar{\Gamma}(\sigma)\)).

Let Polymorphism

There is only one rule to introduce polymorphic type into the context Γ:

Γ⊢e:σ       Γ,x:σ⊢e':τ 
  Γ⊢(let x=e in e'):τ
Continue reading

May 10, 2015 - SAT solving puzzles

Few months ago, Cheryl birthday puzzle has has been an internet phenomenon. If you found the puzzle tricky to solve, we are in the same boat. However, if you observe, the puzzle only requires us to apply simple logic; not number theory or complex arithmetic, just simple logic. What, then, makes the puzzle tricky?

I attribute its trickiness to the chain of reasoning involved - repeated application of simple logic to the existing knowledge to make new deductions until we arrive at the solution. Since the reasoning is quite involved, it would be great if we can enlist the services of a computer to help us in the process. But, how can a computer assist us in making deductions? The answer lies in the well-known SAT problem.

Knights and Knaves Puzzle

Consider the following simple instance of the famous Knights and Knaves class of puzzles:

There is an island in which certain inhabitants, called knights
always tell the truth, and others, called knaves always lie. It is
assumed that every inhabitant of this island is either a knight or 
a knave. 

Suppose A says, “Either I am a knave or B is a knight.” 

What are A and B?

The puzzle is easy to solve mentally. Nonetheless, if you have a 2-SAT solver handy, you can also let solver do the work. Here is how:

Let AisKnight and BisKnight be boolean variables, denoting the propositions “A is a Knight”, and “B is a Knight”, respectively. Since an inhabitant can either be Knight or Knave but not both, boolean formulas ¬ AisKnight and ¬ BisKnight denote the propositions that “A is a Knave”, and “B is a Knave”, respectively.

Now, consider the statement made by A: “Either I am a knave or B is a knight”. Symbolically, it is equivalent to: (¬ AisKnight) ∨ BisKnight. Since Knights always speak truth, and Knaves always lie, the statement is true if A is a Knight, and false if A is a Knave. In other words, the statement holds if and only if A is a Knight. Symbolically, it means:

AisKnight ⇔ (¬ AisKnight) ∨ BisKnight

Observe that the above boolean formula completely describes the constraints imposed by the puzzle, and does so quite succinctly. If the above formula is satisfiable, then the constraints imposed by the puzzle are also satisfiable, which means that puzzle has a solution. Furthermore, the satisfying assignment to literals in the formula (i.e., their truth values) give us the solution to the puzzle. To get those satisfying assignments is what the 2-SAT solver is for. If we feed the above formula to a 2-SAT solver, we get AisKnight = trueand BisKnight = true as satisfying assignments, telling us that A and B are both knights.

Note that satisfying assignment only tells us that “if A is knight, then the puzzle is solved”. Maybe the puzzle is also solved if A is a knave. How do we check for this possibility? Again, using the solver. We explicitly encode the constraint that A is Knave, and ask if our constraints are satisfiable. The boolean formula is shown below:

(AisKnight ⇔ (¬ AisKnight) ∨ BisKnight) ∧ (¬ AisKnight)

A 2-SAT solver cannot find any satisfying assignment to the above formula, indicating that our constraints are unsatisfiable. Hence, A can never be a Knave.

Now, lets take a step back and summarize what we have done. We were given a puzzle that is not difficult, but not obvious either. Instead of doing the reasoning ourselves, we simply described the puzzle as a boolean formula, and let a SAT solver do the reasoning for us. In other words, we have outsourced the reasoning to a solver.This facility to outsource some or all of the reasoning to a solver can be quite handy when we are solving logical puzzles that require more complex reasoning, like Cheryl’s birthday puzzle.

Continue reading