proof.tex

Researchers~\cite{pldi14,maximal} propose two axioms, {\em prefix closedness} and {\em local determinism}, which we adapt to establish our feasibility guarantee. 
Suppose $\mathcal{F}$ denotes the domain of feasible traces.


Intuitively, Prefix closedness means that if a trace is feasible, then the trace is still feasible after we discard the events after a point. The underlying reason is that the events after a point cannot affect the events before it. More formally,

\begin{myaxiom}[Prefix closedness]~\label{axiom:prefix}
If $t_1$ $t_2$ $\in \mathcal{F}$, then $t_1 \in \mathcal{F}$. 
\end{myaxiom}




Intuitively, local determinism says that only the previous events of the same thread determine the existence of an event. For example, the existence of an event is only determined by the branch  thread-locally. However, the value read by an event may be affected by another thread because a shared read reads from the most recent write, which may come from a different thread. The value in other events, such as branch or write,  are locally determined too.
More formally,





\begin{myaxiom}[Local determinism]~\label{axiom:local}
Assume $t_1e_1, t_2 \in \mathcal{F}$, and $t_1|thread(e_1)\approx t_2|thread(e_1)$, where $\approx$ denotes the two traces are equal if the data values in the read and write events are ignored, 
Each event is determined by the previous events in the same thread. There are four cases:
\begin{itemize}
%TODO refine it.
\item {\bf Branch\ }. If op($e_1$)=branch, and $e_1$ is in the form of $x<y$ (without loss of generality), then there exists values $v_x$, $v_y$ such that $t_2 e_1 [v_x/data_x, v_y/data_y] \in \mathcal{F}$. Here $e_1 [v_x/data_x]$ represents that we replace the value of $x$ from $data_x$ to $v_x$ in $e_1$.
\item {\bf Read\ }. If op($e_1$)=read, and $e_2$ is a read event that is identical to $e_1$ except that it may read a different value, and $t_2 e_2$ is consistent, then $t_2 e_2 \in \mathcal{F}$.
\item {\bf Write\ }. If op($e_1$)=write, and there is a value $v$ such that $t_2 e_1[v/data]\in \mathcal{F}$. 
\item {\bf Others \ }. If op($e_1$) is of type different from above and $t_2 e_1$ is consistent, then $t_2 e_1 \in \mathcal{F}$.
\end{itemize}

Here, the consistency is defined as follows. 
A trace is consistency iff it satisfies (1) read-write consistency, i.e., read event should contain the value written by the most recent write event, and (2) the synchronization consistency, e.g., the lock acquire and release of a lock should not be interleaved by the lock operations of the same lock, the begin event of a thread should follow the fork event of the parent thread.
\end{myaxiom}

The local determinism resembles the version in ~\cite{pldi14,maximal}. A crucial difference is that, for the branch event, we do not require all reads thread locally before it to read the identical values as in the original trace $t_1 e_1$. Instead, we allow the previous reads to read different values as long as the branch event is evaluated to the same boolean value, which guarantees the existence of the following events. Such relaxation allows us to find more races, while still preserving the feasibility. 


An important assumption of ours is, we assume all local accesses are recorded in the trace so that we can determine the boolean status of a branch event computationally. ~\cite{pldi14}, which assume the local accesses are not recorded and cannot determine the status computationally, have to enforce the reads before a branch to read the same values, leading to a weaker feasibility criterion. We believe our axiom captures the real-world scenario more faithfully.
Another important assumption is for the read-write consistency, i.e., we assume the heap invariant, so that we know exactly which reads correspond to which writes in the predicted run.

%\begin{myaxiom}
%A set of traces $\mathcal{F}$ is feasible if it satisfies prefix closedness and local determinism axioms. 
%\end{myaxiom}



They are called axioms because they are the rules that the sequentially consistent system~\cite{maximal} should follow.
We refer the readers to the detailed discussion~\cite{maximal, pldi14}.



%TODO what is \Phi
\begin{mytheorem}[Soundness]
All traces in the closure $closure(t, \Phi)$, which includes $t$ and is closed under the derivations in Axioms~\ref{axiom:prefix}~\ref{axiom:local}, are feasible.
\end{mytheorem}

%$\theta_1(expr(e_1))=\theta_2(expr_{e_1})$, then $t_2 \e_1 \in \mathcal{F}$. Here $\theta_1, \theta_2$ represent the mappings between variables and values established prior to $e_1$ by the same thread $thread(e_1)$. $expr(e_1)$ is a helper function that returns the expression in the branch condition. 
\begin{proof}
We order the traces in $closure(t)$ as, $t_0=t, t_1, t_2, t_3, \dots t_n$. Clearly, $t_0$ is feasible. In the following, we prove by induction, i.e., assume $t_{n}$ is feasible, then $t_{n+1}$ which is derived from $S=\{t_0, \dots t_n\}$ should be feasible. There are several possible derivations.
\begin{itemize}
\item if $t_{n+1}$ is a prefix of $t'\in S$, then $t_{n+1}\in\mathcal{F}$ because of the prefix closedness. $t_{n+1}$ shares the same mappings as $t'$.
\item if $t_{n+1}$ is derived from $t^1 e^1, t^2\in \mathcal{F}$, we have $t^1|thread(e^1)\approx t^2|thread(e^1)$.
\begin{itemize}
\item $op(e^1)=branch$ and $e^1= x<y$. Our solver computes a mapping $\theta^d$ of all relevant variables such that $\theta(x<y)=\theta^d(x<y)$, then 
$t^2 e_1[\theta^d(x)/\theta(x),\theta^d(y)/\theta(y) ]  \in \mathcal{F}$. Note that the mapping computed by solver may be different from the mapping in the trace $t^1$.
\item $op(e^1)=read$. Our solver ensures the read-write consistency, i.e., $t^2 e^2$ is consistent, then $t^2 e^2 \in \mathcal{F}$. Note that $e^2$ is the same as $e^1$ except that it may read a different value.
\item $op(e^1)=write$. There exists a value $v$ such that $t^2 e^2[v/data]\in \mathcal{F}$, where $v$ is included in the mapping computed by the solver. 
\item $op(e^1)$ is of other types. Our solver ensures the consistency, i.e., $t^2 e^1$ is consistent, then $t^2 e^2 \in \mathcal{F}$.
\end{itemize}
\end{itemize}
\end{proof}



\begin{mytheorem}[Maximality]
$\forall t', s.t., t'|th\approx t|th for any thread th, if t'\notin closure(t,\Phi), t' is infeasible.$
\end{mytheorem}

\begin{proof}
We sketch the proof. All traces that satisfy  $t'|th\approx t|th for any thread th$ 
\end{proof}



%discussion.