Strong consistency increases latency; weak consistency is hard to reason about. Compromising between the two, a number of databases allow each operation to run with either strong or weak consistency. Ideally, users choose the minimal set of strongly consistent operations needed to enforce some application specific invariant. However, deciding which operations to run with strong consistency and which to run with weak consistency can be very challenging. This paper

 - introduces a formal hybrid consistency model which subsumes many existing consistency models,
 - introduces a modular proof rule which can determine whether a given consistency model enforces an invariant, and
 - implements a prototype using a standard SMT solver.

Consistency Model, Informally. Consider

 - a set of states $s, s_{init} \in$ State,
 - a set of operations Op = {o, ...},
 - a set of values $\bot$ in Val, and
 - a set of replicas $r_1, r_2,$ ....

The denotation of an operation is denoted F_o where

 - F_o: State -> (Val x (State -> State)),
 - F_o^val(s) = F_o(s)[0] (the value returned by the operation), and
 - F_o^eff(s) = F_o(s)[1] (the effect of the operation).

For example, a banking operation may let states range over natural numbers where

 - F_deposit_a(s) = (\bot, fun s' -> s' + a)
 - F_interest(s) = (\bot, fun s' -> s' + 0.05 * s)
 - F_query(s) = (s, fun s' -> s')

If all operations commute (i.e. forall o1, o2, s1, s2. F_o1(s1) o F_o2(s2) = F_o2(s2) o F_o1(s1)), then all replicas are guaranteed to converge. However, convergence does not guarantee all application invariants are maintained. For example, an invariant I = {s | s >= 0} could be violated by merging concurrent withdrawals. To enforce invariants, we introduce a token system which can be used to order certain operations.

A token system TS = (Token, #) is a set of tokens Token and a symmetric relation # over Token. We say two sets of tokens T1 # T2 if exists t1 in T1, t2 in T2. t1 # t2. We also update our definition of operations to acquire tokens:

 - F_o: State -> (Val x (State -> State) x P(Token)),
 - F_o^val(s) = F_o(s)[0] (the value returned by the operation),
 - F_o^eff(s) = F_o(s)[1] (the effect of the operation), and
 - F_o^tok(s) = F_o(s)[2] (the tokens acquired by the operation).

Our consistency model will ensure that two operations that acquire conflicting operations will be ordered.

Formal Semantics. Recall a strict partial order is a partial order that is transitive and irreflexive (e.g. sets ordered by strict subset). Given a partial order R, we say (a, b) \in R or a -R-> b. Consider a countably infinite set Event of events ranged over by e, f, g. If operations are like transactions, an event is like applying a transaction at a replica.

- Definition 1. Given token system TS = (Token, #), an execution is a tuple X = (E, oper, rval, tok, hb) where
   - E \subset Event is a finite subset of events,
   - oper: E -> Op designates the operation of each event,
   - rval: E -> Val designates the return value of each event,
   - tok: E -> P(Token) designates the tokens acquired by each event, and
   - hb \subset Event x Event is a happens before strict partial order where forall e, f. tok(e) # tok(f) => (e-hb->f or f-hb->e).

An execution formalizes operations executing at various replicas concurrently, and the happens before relation captures how these operations are propagated between replicas. The transitivity of the happens before relation ensures at least causal consistency.

Let

 - Exec(TS) be the set of all executions over token system TS, and
 - ctxt(e, X) = (E, X.oper|E, X.rval|E, X.tok|E, X.hb|E) be the context of e where E = X.hb^-1(e). Intuitively, ctxt(e, X) is the subexection of X that only includes operations causally preceding e.

Executions are directed graphs of operations, but without a semantics, they are rather meaningless. Here, we define a relation evald_F \subset Exec(TS) x P(State) where evald_F(Y) is the set of all final states Y can be in after all operations are propagated to all replicas. We'll see shortly that if all non-token-conflicting operations commute, then evald_F is a function.

 - evald_F(Y) = {} if Y.E = {}, and
 - evald_F(Y) = {F_e^eff(s)(s') | e \in max(Y), s \in evald_F(ctxt(e, Y)), s' \in evalfd_F(Y|Y.E - {e})} otherwise.

Now

 - Definition 2. An execution X \in Exec(TS) is consistent with TS and F denoted X |= TS, F if forall e \in X.e. exists s \in evald_F(ctxt(e, x)). X.val(e) = F_X.oper(e)^val(s) and X.tok(e = F_X.oper(e)^tok(s)).

We let Exec(TS, F) = {X | X |= TS, F}. Consistent operations are closed under context. Furthermore, evald_F is a function when restricted to consistent executions where non-token-conflicting operations commute. We call this function eval_F.

This model can model a number of consistency models:

 - Causal consistency. Let Token = {}.
 - Sequential consistency. Let Token = {t}, t # t, and F_o^tok(s) = {t} for all o.
 - RedBlue Consistency. Let Token = {t}, t # t, and F_o^tok(s) = {t} for all red o and F_o^tok(s) = {} for all blue o.

State Based Proof Rule. We want to construct a proof rule to establish the fact that Exec(TS, F) \subset eval_F^-1(I). That is, every execution results in a state that satisfies the invariant. Since executions are closed under context, this also means that all operations execute on a state that satisfies the invariant.

Our proof rule involves a guarantee relation G(t) over states which describes all possible state changes that can occur while holding token t. Similarly, G_0 describes the state transitions that can occur without holding any tokens.

Here is the proof rule.

 - S1: s_init \in I.
 - S2: G_0(I) \subset I and forall t. G(t)(I) \subset I.
 - S3: forall o, s, s'.
    - s \in I and
    - (s, s') \in (G_0 \cup G(F_o^tok(s)^\bot))* =>
    - (s', F_o^eff(s)(s')) \in G_0 \cup G(F_o^tok(s)).


In English,

 - S1: s_init satisfies the invariant.
 - S2: G and G_0 preserve the invariant.
 - S3: If we start in any state s that satisfies the invariant and can transition in any finite number of steps to any state s' without acquiring any tokens conflicting with o, then we can transition from s' to F_o^eff(s)(s') in a single step using the tokens acquired by o.

Event Based Proof Rule and Soundness. Instead of looking at states, we can instead look at executions. That is, if we let invariants I \subset Exec(TS), then we want to write a proof rule to ensure Exec(TS, F) \subset I. That is, all consistent executions satisfy the invariant. Again, we use a guarantee G \subset Exec(TS) x Exec(TS).

 - E1: X_init \in I.
 - E2: G(I) \in I.
 - E3: forall X, X', X''. forall e in X''.E.
    - X'' |= TS, F and
    - X' = X''|X''.E - {e} and
    - e \in max(X'') and
    - X = ctxt(e, X'') and
    - X \in I and
    - (X, X') \in G* =>
    - (X', X'') \in G.

This proof rule is proven sound. The event based rule and its soundness is derived from this.

Examples and Automation. The authors have built a banking, auction, and courseware application in this style. They have also built a prototype that you give TS, F, and I and it determines if Exec(T, f) \subset eval_F^-1(I). Their prototype modifies the state-based proof rule eliminating the transitive closure and introducing intermediate predicates.

In 1980, synchronization primitives like semaphores, monitors, and condition variables had been well studied in the literature, but there weren't any large systems implementing them. Mesa was a programming language that was being developed to write the Pilot operating system at Xerox. Due to the inherent concurrency of an operating system, Mesa was designed to ease the development of concurrent programs. The Mesa designers considered implementing a message passing interface, but deemed it too complex. They considered semaphores, but found them too undisciplined. They considered cooperative multi-threading but came upon a number of serious disadvantages:

 - Cooperative multithreading cannot take advantage of multiple cores.
 - Preemption is already required to service time-sensitive I/O devices.
 - Cooperation is at odds with modularity. Critical sections have no principled way of knowing if they are calling a function which yields control.

Eventually, Mesa settled on implementing monitors and condition variables and exposed a number of previously undiscussed issues:

 - What is the interface for dynamically spawning threads and waiting for them to terminate?
 - What is the interface for dynamically constructing monitors?
 - How are threads scheduled when waiting and notifying each other?
 - What are the semantics of wait when one monitor calls into another monitor which also calls wait?
 - How are exceptions and I/O devices handled?

Mesa allowed an arbitrary function call to be forked and run by a separate thread and eventually joined:


https://i.imgur.com/McaDktY.png

Moreover, if a forked thread was not intended to be joined, it could instead be detached via detach[p]. This fork/join style process management had a number of advantages---(i) processes were first class values, (ii) thread forking was type checked, and (iii) any procedure could be forked---but also introduced lots of opportunities for dangling references.

Monitors are objects that only allow a single thread to be executing one of its functions at any given time. They unify data, synchronization of the data, and access of the data into one lexical bundle. Mesa monitors included public entry preocedures and private internal procedures that operated with the monitor locked as well as public external procedures that operated without locking the monitor. Monitors, in conjunction with condition variables, were used to maintain an invariant about an object that was true upon entering and exiting any of the monitor's methods. Monitors also lead to potential deadlocks:

 - Two monitor methods could wait for one another.
 - Two different monitors could enter each other.
 - A monitor M could enter a monitor N, then wait on a condition that could only be enabled by another thread entering M through N.


Special care also had to be taken to avoid priority inversion.

Mesa also introduced Mesa semantics, best explained with this code snippet:

```
"""
Condition variables typically obey one of two semantics:

1. Under *Hoare semantics* [1], when a thread calls `notify` on a condition
   variable, the execution of one of the threads waiting on the condition
   variable is immediately resumed. Thus, a thread that calls `wait` can assume
   very strong invariants are held when it is awoken.
2. Under *Mesa semantics* [2], a call to `notify` is nothing more than a hint.
   Threads calling `wait` can be woken up at any time for any reason.

Understanding the distinction between Hoare and Mesa semantics can be
solidified by way of example. This program implements a concurrent queue (aka
pipe) to which data can be written and from which data can be read. It spawns a
single thread which iteratively writes data into the pipe, and it spawns
`NUM_CONSUMERS` threads that read from the pipe. The producer produces the same
number of items that the consumers consume, so if all goes well, the program
will run and terminate successfully.

Run the program; not all goes well:

    Exception in thread Thread-3:
    Traceback (most recent call last):
      File "/usr/lib/python2.7/threading.py", line 810, in __bootstrap_inner
        self.run()
      File "/usr/lib/python2.7/threading.py", line 763, in run
        self.__target(*self.__args, **self.__kwargs)
      File "hoare_mesa.py", line 66, in consume
        pipe.pop()
      File "hoare_mesa.py", line 52, in pop
        return self.xs.pop(0)
    IndexError: pop from empty list

Why? The pipe is implemented assuming Python condition variables obey Hoare
semantics. They do not. Modify the pipe's implementation assuming Mesa
semantics and re-run the program. Everything should run smoothly!

[1]: https://scholar.google.com/scholar?cluster=16665458100449755173&hl=en&as_sdt=0,5
[2]: https://scholar.google.com/scholar?cluster=492255216248422903&hl=en&as_sdt=0,5
"""

import threading

# The number of objects read from and written to the pipe.
NUM_OBJECTS = 10000

# The number of threads consuming from the pipe.
NUM_CONSUMERS = 2

# An asynchronous queue (a.k.a. pipe) that assumes (erroneously) that Python
# condition variables follow Hoare semantics.
class HoarePipe(object):
    def __init__(self):
        self.xs = []
        self.lock = threading.Lock()
        self.data_available = threading.Condition(self.lock)

    # Pop the first element from the pipe, blocking if necessary until data is
    # available.
    def pop(self):
        with self.lock:
            # This code is incorrect beacuse Python condition variables follows
            # Mesa, not Hoare, semantics. To correct the code, simply replace
            # the `if` with a `while`.
            if len(self.xs) == 0:
                self.data_available.wait()
            return self.xs.pop(0)

    # Push a value to the pipe.
    def push(self, x):
        with self.lock:
            self.xs.append(x)
            self.data_available.notify()

def produce(pipe):
    for i in range(NUM_OBJECTS):
        pipe.push(i)

def consume(pipe):
    assert NUM_OBJECTS % NUM_CONSUMERS == 0
    for i in range(NUM_OBJECTS / NUM_CONSUMERS):
        pipe.pop()

def main():
    pipe = HoarePipe()
    producer = threading.Thread(target=produce, args=(pipe,))
    consumers = [threading.Thread(target=consume, args=(pipe,))
                 for i in range(NUM_CONSUMERS)]

    producer.start()
    for consumer in consumers:
        consumer.start()

    producer.join()
    for consumer in consumers:
        consumer.join()

if __name__ == "__main__":
    main()
```

Threads waiting on a condition variable could also be awoken by a timeout, an abort, or a broadcast (e.g. notify_all).

Mesa's implementation was divided between the processor, a runtime, and the compiler. The processor was responsible for process management and scheduling. Each process was on a ready queue, monitor lock queue, condition variable queue, or fault queue. The runtime was responsible for providing the fork/join interface. The compiler performed code generation and a few static sanity checks.

Mesa was evaluated by Pilot (an OS), Violet (a distributed calendar), and Gateway (a router).

## General Framework
Really **similar to DAgger** (see [summary](https://www.shortscience.org/paper?bibtexKey=journals/corr/1011.0686&a=muntermulehitch)) but considers **cost-sensitive classification** ("some mistakes are worst than others": you should be more careful in imitating that particular action of the expert if failing in doing so incurs a large cost-to-go). By doing so they improve from DAgger's bound of $\epsilon_{class}uT$ where $u$ is the difference in cost-to-go (between the expert and one error followed by expert policy) to  $\epsilon_{class}T$ where $\epsilon_{class}$ is the error due to the lack of expressiveness of the policy class. In brief, by accounting for the effect of a mistake on the cost-to-go they remove the cost-to-go contribution to the bound (difference in the performance of the learned policy vs. expert policy) and thus have a tighter bound. In the paper they use the word "regret" for two distinct concepts which is confusing to me: one for the no-regret online learning meta-approach to IL (similar to DAgger) and another one because Aggrevate aims at minimizing the cost-to-go difference with the expert (cost-to-go difference: the sum of the cost I endured because I did not behave like the expert once = *regret*) compared to DAgger that aims at minimizing the error rate wrt. the expert.

Additionally, the paper extends the view of Imitation learning as an online learning procedure to Reinforcement Learning. 

## Assumptions
**Interactive**: you can re-query the expert and thus reach $\epsilon T$ bounds instead of $\epsilon T^2$ like with non-interactive methods (Behavioral Cloning) due to compounding error.
Additionally, one also needs a **reward/cost** that **cannot** be defined relative to the expert (no 0-1 loss wrt expert for ex.) since the cost-to-go is computed under the expert policy (would always yield 0 cost).

## Other methods
**SEARN**: does also reason about **cost-to-go but under the current policy** instead of the expert's (even if you can use the expert's in practice and thus becomes really similar to Aggrevate). SEARN uses **stochastic policies** and can be seen as an Aggrevate variant where stochastic mixing is used to solve the online learning problem instead of **Regularized-Follow-The-Leader (R-FTL)**. 

## Aggrevate - IL with cost-to-go
![](https://i.imgur.com/I1otJwV.png)

Pretty much like DAgger but one has to use a no-regret online learning algo to do **cost-sensitive** instead of regular classification. In the paper, they use the R-FTL algorithm and train the policy on all previous iterations. Indeed, using R-FTL with strongly convex loss (like the squared error) with stable batch leaner (like stochastic gradient descent) ensures the no-regret property.

In practice (to deal with infinite policy classes and knowing the cost of only a few actions per state) they reduce cost-sensitive classification to an **argmax regression problem** where they train a model to match the cost given state-action (and time if we want nonstationary policies) using the collected datapoints and the (strongly convex) squared error loss. Then, they argmin this model to know which action minimizes the cost-to-go (cost-sensitive classification). This is close to what we do for **Q-learning** (DQN or DDPG): fit a critic (Q-values) with the TD-error (instead of full rollouts cost-to-go of expert), argmax your critic to get your policy. Similarly to DQN, the way you explore the actions of which you compute the cost-to-go is important (in this paper they do uniform exploration).

**Limitations**

If the policy class is not expressive enough and cannot match the expert policy performance this algo may fail to learn a reasonable policy. Example: the task is to go for point A to point B, there exist a narrow shortcut and a safer but longer road. The expert can handle both roads so it prefers taking the shortcut. Even if the learned policy class can handle the safer road it will keep trying to use the narrow one and fail to reach the goal. This is because all the costs-to-go are computed under the expert's policy, thus ignoring the fact that they cannot be achieved by any policy of the learned policy class. 

## RL via No-Regrety Policy Iteration -- NRPI
![](https://i.imgur.com/X4ckv1u.png)

NRPI does not require an expert policy anymore but only a **state exploration distribution**. NRPI can also be preferred when no policy in the policy class can match the expert's since it allows for more exploration by considering the **cost-to-go of the current policy**. 

Here, the argmax regression equivalent problem is really similar to Q-learning (where we use sampled cost-to-go from rollouts instead of Bellman errors) but where **the cost-to-go** of the aggregate dataset corresponds to **outdated policies!** (in contrast, DQN's data is comprised of rewards instead of costs-to-go).
Yet, since R-FTL is a no-regret online learning method, the learned policy performs well under all the costs-to-go of previous iterations and the policies as well as the costs-to-go converge. 

The performance of NRPI is strongly limited to the quality of the exploration distribution. Yet if the exploration distribution is optimal, then NRPI is also optimal (the bound $T\epsilon_{regret} \rightarrow 0$ with enough online iterations). This may be a promising method for not interactive, state-only IL (if you have access to a reward).

## General limitations
Both methods are much less sample efficient than DAgger as they require costs-to-go: one full rollout for one data-point.

## Broad contribution 
Seeing iterative learning methods such as Q-learning in the light of online learning methods is insightful and yields better bounds and understanding of why some methods might work. It presents a good tool to analyze the dynamics that interleaves learning and execution (optimizing and collecting data) for the purpose of generalization. For example, the bound for NRPI can seem quite counter-intuitive to someone familiar with on-policy/off-policy distinction, indeed NRPI optimizes a policy wrt to **costs-to-go of other policies**, yet R-FTL tells us that it converges towards what we want. Additionally, it may give a practical advantage for stability as the policy is optimized with larger batches and thus as to be good across many states and many cost-to-go formulations.

#### Introduction

* The paper explains how to apply dropout to LSTMs and how it could reduce overfitting in tasks like language modelling, speech recognition, image caption generation and machine translation.
* [Link to the paper](https://arxiv.org/abs/1409.2329)

#### [Dropout](https://www.cs.toronto.edu/~hinton/absps/JMLRdropout.pdf)

* Regularisation method that drops out (or temporarily removes) units in a neural network.
the network, along with all its incoming and outgoing connections
* Conventional dropout does not work well with RNNs as the recurrence amplifies the noise and hurts learning.

#### Regularization

* The paper proposes to apply dropout to only the non-recurrent connections.
* The dropout operator would corrupt information carried by some units (and not all) forcing them to perform intermediate computations more robustly.
* The information is corrupted L+1 times where L is the number of layers and is independent of timestamps traversed by the information.

#### Observation

* In the context of language modelling, image caption generation, speech recognition and machine translation, dropout enables training larger networks and reduces the testing error in terms of perplexity and frame accuracy.

Yoshua Bengio’s visionary work on probabilistic language modelling had a huge impact on the field of Natural Language Processing. Despite that it was published nearly 20 years ago, it is still relevant to modern NLP solutions. In fact, the subsequent works perfected the state-of-the-art in NLP, although it took more than 10 years for the paper to get a significant attention in the field.

The authors approach the fundamental problem of exponentially growing number of trainable parameters with the size of corpora. The problem is called “Curse of Dimensionality” and limits the generalization performance of conventional approaches such as N-gram models. For instance, if we want to model a joint distribution of 10 consecutive words with a vocabulary of size 100,000, there are potentially 10^50-1 trainable variables.

The proposed probabilistic modeling approach scales linearly with the size of the vocabulary. It comprises of two steps: 1) converting words into real-valued feature vector of size m and 2) extract joint probability of the word sequence represented by the feature vectors (total size of (n-1)-by-m). While the first step is implemented as a trainable matrix of size |V|*m, the joint probability function is implemented as two densely connected layers (tanh and softmax activation) with a skip connection between the input of the first layer and the input of the second layers. The first layer has weight matrix of size m*h and the second is (nm+h)*|V|, which results in total of |V|(1+nm+h)+h(1+(n-1)m) trainable variables. The output of the model is then mixed with the output of a tri-gram model.

As the optimization objective, the authors employ log-likelihood of the next word regularized on the weights of dense layers (biases are excluded, as well as, matrix of real-valued word features embedding matrix of size |V|-by-m). The goal of the optimization is to find the parameters that minimize the perplexity of the training dataset. Eventually we learn the distributed representations of the words and the probability function of a sequence as a function of the distributed word representations.
The proposed model improved the out-of-sample perplexity score by 24% for Brown and 8% on AP news datasets compared to the state-of-the-art smoothed trigram models. The best performing architecture comprised h=100, m=30, without a skip connection, but with trigram mixing.

As a primary drawback of the approach, authors mention significant speed limitations and propose use of shallow networks, time delay and recurrent neural networks to mitigate the problem and improve the performance. They also consider several promising direction for future research such as decomposing the network in sub-networks, representing the conditional probability as a tree, introducing a-priori knowledge, interpretable word embedding, and adjusting the gradient propagation path.

As a critique, the training did not explicitly target word semantics; although the authors claim that their embedding takes advantage of the inherently learned similarity (close words are expected to have similar feature vectors). For example, a better approach could be a Siamese network with an objective to minimize a distance (e.g. cosine or Euclidian) between “similar” words, this would also decrease the number of the trainable variables and well as exclude the risky non-regularized word embedding matrix. Secondly, as the authors mentioned, the model could significantly benefit from use of GRU, RNN, LSTM and other network architectures, as well as including prior knowledge. Finally, the model scales linearly with n and |V|, which significantly limits its application.