trace.tex

\section{Relaxation of Flow Dependencies}
The main goal of our analysis is to, given an original trace $\tau$ over the events $\mathcal{E}$, derive a trace $\tau'$ over the same set of events, which has a new scheduling $\pi$ of the events (the order of events inside each thread should remain unchanged) and a new mapping $\theta$ from variables to values in the events. Our first relaxation comes from the insight that, we allow the variables to read different values than in the original trace even if such variables are used to determine the control flow, while existing approaches enforce them to read the same values as in the original trace. As a result, our relaxation allows more schedules, which are likely to expose more races.
 
Not every scheduling or every mapping $\theta$ guarantees a new feasible trace $\tau'$, therefore, we need to compute the scheduling and mapping that lead to feasible trace. We explain the technique details in the following.


% % 
% TODO: Explain the format of the raw trace in impl.tex.
% %


%We begin by describing the first relaxation, whereby the dependence structure defined by the original trace is potentially violated while retaining soundness.

\subsection{SSA Form of the Trace}
First of all, we require the SSA form of the trace, i.e., each variable in defined exactly once in the trace. Such requirement is a prerequisite for the computation of the mapping $\theta$, as it can map each variable to only one value. Another side effect is that the def/use chains become explicit in the SSA form, which simplifies the following analysis steps.

\tool\ handles the local assignment and heap accesses differently.
\begin{itemize}
\item {\bf Local Assignment\ } The SSA form for local assignment resembles the SSA form of static instructions in compiler optimization, except that the loops and recursions are fully resolved in a concrete trace and there is no need for the Phi node. More concretely, we replace the variable $v$ defined in an event, as well as the following uses of the definition, to a new variable $v^{id}$, where $id$ is the unique id of the event. The uniqueness of the id guarantees that no two events define the same variable, i.e., each variable is defined exactly once. Note that the uses of a definition can be computed easily by scanning the trace afterwards for the variables of the same name before the next redefinition. 
\item {\bf Heap accesses\ } The accesses of the local heap locations and the accesses of shared locations behave differently, therefore, we introduce different SSA form for them. 
\begin{itemize}
\item {\bf Local Heap Accesses\ } The accesses of local heap locations behave similarly to the local assignment as both the definition and uses belong to the single thread. Therefore we model them as local assignments: We introduce a fresh local variable {\tt l$_{\lsyn o.f \rsyn}^{id}$} to replace each definition and  the corresponding uses of a  field {\tt f} of the local object $o$. An assumption here is the uses and the definition still refer to the same base object $o$ in the predicted run, which is enforced through the constraint specification (Section~\ref{sec:...}).
\item  {\bf Shared Heap Accesses\ } The accesses of shared locations are more complex. Each shared read may read from one of multiple writes that define the shared location, under different schedules.     Given the write $x.f=y$ or the read $y=x.f$, we introduce two symbols, $W^{id}_{\tt x.f }$, which denotes the write access by the event $id$ to the field $f$ of the shared object referenced by $x$, and $R^{id}_{\tt  x.f }$,  which denotes the read access  by the event $id$ to the location $x.f$.  Note that, $x.f$ in the subscript is interpreted as the location, denoted as a pair $(\lsyn x \rsyn^e, f)$, rather than the value stored in the location. 
Similar to the local heap accesses, an assumption for the correlation is that the writes and reads still refer to the same base object $o$ in the predicted run, which we guarantee by specifying additional constraints (Section~\ref{sec:...}). 
\end{itemize}
\end{itemize}

% We could encode the question of shared versus local accesses as additional constraints (requiring that a variable be accessed by more than one thread), but that would be more complicated and less efficient.


%\paragraph{Basic Encoding: Local Accesses}
%
%The fundamental encoding transformation is to induce Static Single Assignment (SSA) form on the raw trace, such that
%a variable is defined exactly once. In this way, , and encoding of trace events as constraints is simplified. As an illustration, trace
%\begin{quote}
%	{\tt 1: x=1; 2: x<3; 3: x=3;} \\
%	{\tt 4: y=1;} \\
%	{\tt 5: z=x+y}
%\end{quote}
%becomes
%\begin{quote}
%	{\tt 1: x$^1$=1; 2: x$^1$<3; 3: x$^3$=3;} \\
%	{\tt 4: y$^4$=1;} \\
%	{\tt 5: z$^5$=x$^3$+y$^4$}
%\end{quote}
%(For readability, we version variables according to the line number of their definition.)



%%TODO update the intro+moti, make sure the same style
\begin{figure}
\centering
\begin{tabular}{ll}
\multicolumn{2}{c}{{\tt {\bf x} = 0; {\bf y} = 0;}} \\
\hline
\multicolumn{1}{c}{$T_1$} & \multicolumn{1}{c}{$T_2$} \\
\hline
{\tt 1: s=0; } & \\
{\tt 2: for(i=1;i<3;i++)} & \\
{\tt 3: \ \ \ s+=i;} & \\
{\tt 4: {\bf y} = s;} & \\
{\tt 5: {\bf x} = 1;} & \\
{\tt 6: {\bf y} = 5;} & \\
& {\tt 7: if ({\bf y} > 2)} \\
& {\tt 8:~~print({\bf x}+1);} \\	
& {\color{Gray} {\tt 9: else}} \\
& {\color{Gray} {\tt 10:~~print({\bf x}+2);}}
\end{tabular}
\caption{Running Example (shared variables are in bold font). }
\label{fig:running2}
\end{figure}

 
\begin{figure}
\centering
\begin{tabular}{l|l}
\hline
\multicolumn{1}{c}{$Trace$} & \multicolumn{1}{c}{$SSA \ form \ of\   Trace$} \\
\hline
{\tt 0: {\bf x}=0} &  {\tt 0: $W^0_x$=0}    \\
{\tt 1: {\bf y}=0} &   {\tt 1: $W^1_y$=0}   \\
{\tt 2: s=0} &  {\tt 2: $s^2$=0}   \\
{\tt 3: i=1} &     {\tt 3: $i^3$=1}   \\
{\tt 4: i<3} &    {\tt 4: $i^3$<3} \\
{\tt 5: s=s+i} & {\tt 5: $s^5$=$s^2$+$i^3$}   \\
{\tt 6: i=2} &       {\tt 6: $i^6$=2}  \\
{\tt 7: i<3} &      {\tt 7: $i^6$<3}  \\
{\tt 8: s=s+i} &  {\tt 8: $s^8$=$s^5$+$i^6$}  \\
{\tt 9: i=3} &     {\tt 9: $i^9$=3}  \\
{\tt 10: i<3} &    {\tt 10: $i^9$<3}  \\
{\tt 11: {\bf y} = s;} &  {\tt 11: $W^{11}_y$ = $s^8$;}  \\
{\tt 12: {\bf x} = 1;} &    {\tt 12: $W^{12}_x$ = 1;}   \\
{\tt 13: {\bf y} = 5;} &    {\tt 13: $W^{13}_y$ = 5;}  \\
{\tt 14: {\bf y} > 2}  &    {\tt 14: $R^{14}_y$ > 2} \\
{\tt 15: tmp={\bf x}+1;}  & {\tt 15: tmp=$R^{15}_x$+1;}   \\	
{\tt 16: print(tmp);} &  {\tt 16: print(tmp);}  \\
\end{tabular}
\caption{Trace}
\label{fig:t4running2}
\end{figure}

Figure~\ref{fig:t4running2} exemplifies a trace and its SSA form, where the trace is generated from the program in Figure~\ref{fig:running2}.
Each label in  Figure~\ref{fig:t4running2} on the left hand denotes the id of the event. As seen, event 5 uses the variable $s^2$ defined at event 2 and defines the variable $s^5$, which is used afterwards. The read/write of the shared variables are denoted in the special form, such as $R^{14}_y$ and $W^{13}_y$. We use $x, y$ to represent the location for simplicity.



%TODO value or symbol for o.f, rethink about it.
\subsection{Constraint System}
Based on the SSA form of the trace, we build the constraints to compute a new trace with the new schedule and new mapping of variables to values.
To model the schedule, we introduce the order variable $O_{e}$ for each event $e$. Given two events $e_i, e_j$ from two different threads, $O_{e_i}<O_{e_j}$ in a trace means $e_i$ is scheduled before $e_j$. We omit the synchronization constraints purposely, which are well explained in all existing predictive analysis techniques~\cite{yannis, pldi14}.

%TODO synchronization constraint


%Having explained how the trace is encoded, we now describe in detail how constraints are derived from the trace, such that any permutation considered by the analysis is guaranteed to represent a feasible execution schedule.

{\bf Race Condition\ } Given any pair  of events, $e$ and $e'$,  that both access a common memory location $l$, we demand that
$$
\begin{array}{rl}
& t^e \neq t^{e'} \\
\bigwedge 	& (e\  writes\  l\   \vee e'\  writes\  l) \\
\bigwedge   & O_{e} = O_{e'}
\end{array}
$$
That is, (i) events $e$ and $e'$ are executed by different threads, (ii) at least one of the events performs write access to $l$, and (iii) the events run concurrently. This is a direct logical encoding of the definition of a race condition. We refer to both $e$ and $e'$ as the racy event.

{\bf Intra-thread Constraints\ } Given a racy pair under analysis, $e$ and $e'$, suppose $e$ is after $e'$ in the original trace $\tau$, the predictive analysis reschedules the events in the prefix of $e$, i.e., prior to $e$, so that $e$ and $e'$ can run concurrently. A necessary condition applied to predictive analysis techniques is that each thread should follow the same event sequence prior to $e$ as in the original run.  We explain the rationale underlying this requirement in Section~\ref{sec:proof}, but now proceed to explain how to guarantee it using constraints. The preservation of the event sequence for each thread requires the intra-thread constraints:

\begin{itemize}
\item {\bf Branch Decision Constraints\ } The branches in the prefix should take the same decisions to reproduce the same set of events. More formally,  
we require that 
$$
\bigwedge_{e_i \in \tau|\leq e \wedge  inst^{e_i}=x<y.\ }  x<y 	\equiv \lsyn x<y \rsyn^{e_i}
$$ 
where $e_i$ is a branch event of which the boolean expression is $x<y$ (we use the binary operator $<$ for illustration) and  $\lsyn x<y \rsyn^{e_i}$ stores the  evaluation result of the boolean expression in the original trace $\tau$. The constraint specifies that the boolean expression in the derived trace should be evaluated to the same boolean value. Importantly, different from existing analyses \cite{yannis,pldi14}, we do not pose the requirement that the values flowing into branching statements remain the same, but suffice with the relaxed requirement that the evaluation of branching expressions remain the same. For example, suppose  the branch event $x<y$ takes the value $1<2$ in the original trace, existing analyses require the same values for the variables $x$ and $y$ in the predicted run, while we allow  the branch event to take other values of the variables, such as $3<4$. 
\item {\bf Intra-thread Order Constraints\ } The events in the sequence should follow the same order as in the original trace. More formally, we require that
$$
\begin{array}{rl}
\forall e_i, e_j \in \tau. & t^{e_i}\equiv t^{e_j}. \\
& i^{e_i} < i^{e_j}\  \Rightarrow O_{e_i} < O_{e_j}
\end{array}
$$ 
The constraint specifies that the two events from the same thread should follow the same order as reflected by the ids of the events.
\item {\bf Assignment Constraints\ } The mapping of local variables should not contradict each instruction.   More formally, we require that
$$
\bigwedge_{e_i \in \tau|<=e \wedge type(e_i)=assign|heapr|heapw}\
	inst^{e_i}
$$
where $inst^{e_i}$, such as $x=y+z$ or $R^{id}_{x}=y$, captures the constraint over the values of the variables imposed by the instruction. For example, $x=y+z$ is not satisfied if the solver computes a mapping from the three variables to $3, 4, 5$ respectively. Again we consider only the events in the prefix $\tau|e$, where $e$ is the racy event that happens later. Specially, for the instruction involving object creation, $x=new (...)$, we encode the object as its address, i.e., a constant integer returned by $System.identityHashcode(x)$ at runtime.
\end{itemize}




{\bf Rescheduling through Relaxation of Flow Dependencies\ } We now move to the novel feature of \tool, which is its ability to explore execution schedules that depart from the value flow exhibited in the original trace. More precisely, \tool\ is able to relax value flow dependencies in the original trace, whereby a thread reads a
different value possibly written by other events (or even events from other threads) to the shared memory location, while enforcing feasibility.
 This is strictly beyond the coverage potential of existing predictive analyses, which restrict trace transformations to ones where any read access to a shared memory location must correspond to the same written values as in the original trace, which are usually from the same write events. 

To ensure feasibility under relaxation of flow dependencies, we need to secure the flow between the read/write with the execution schedule. 
For example, in Figure \ref{fig:running}, for the read access to ${\tt y}$ at line {\tt 4} obtains the value assigned to ${\tt y}$ at line {\tt 1}, we need the schedule where  thread $T_1$ executes line {\tt 1}, then $T_2$ executes line {\tt 4}, and then the schedule switches again to $T_1$ to execute line {\tt 3}.


% $R_{\tt y}^4={\tt y}^1 \wedge O_1 < O_4 < O_3$ specifies that in a schedule , the $R_{\tt y}^4={\tt y}^1$.

%TODO l and ell
In general, the constraint formula, given read $R_{\ell}$ of location $\ell$ as part of event $e$ with set ${\cal W}$ of matching write events (i.e., events including write access to $\ell$), takes the following form:
$$
\begin{array}{rll}
\bigvee_{e_w \in {\cal W}} &  & (R^{e}_{\ell} = W^{e_w}_{\ell}) \\
&		\bigwedge 	&  O(e_w) < O(e) \\
&		\bigwedge_{e' \in {\cal W} \setminus \{ e_w \}} & (O(e') < O(e_w) \vee O(e) < O(e'))
\end{array}
$$
This disjunctive formula iterates over all matching write events, and demands for each that (i) it occurs prior to the read event ($O(e_w) < O(e)$) and (ii) all other write events either occur before ($O(e') < O(e_w)$) it or after the read event
($O(e) < O(e')$).

An important concern that arises due to relaxation of flow dependencies is that heap accesses may change their meaning, i.e., they involve different base objects and do no longer match with each other. As an illustration, we refer to Figure \ref{fig:heapAccess}. While the read at event {\tt 7} appears to match the write at event {\tt 5}, this is conditioned on the read at event {\tt 6} being linked to the assignment at event {\tt 4}. If the predicted run violates this link, then feasibility is no longer guaranteed. In particular, if reordering results in {\tt z} being assigned the first rather than second allocated object, then the read at event {\tt 7} no longer matches the write  at event {\tt 5}.

\begin{figure}
	\centering
	\begin{tabular}{ll}
		\hline
		\multicolumn{1}{c}{$T_1$} & \multicolumn{1}{c}{$T_2$} \\
		\hline
		{\tt 1: x1 = new();} & \\
		{\tt 2: x2 = new();} & \\
		{\tt 3: y = x1;} & \\
		{\tt 4: y = x2;} & \\
		{\tt 5: x2.f = 5;} & \\	
		& {\tt 6: z = y;} \\
		& {\tt 7: w = z.f;} \\
	\end{tabular}
	\caption{\label{fig:heapAccess}Example illustrating the need to account for heap accesses during trace transformation, where the labelled number denotes the event id.}
\end{figure}

To address this challenge, we enhance the constraint system with the requirement that heap objects that are dereferenced in the following field reference before the candidate racing events retain their original address in the predicted trace.
This achieves two guarantees: First, matching heap access events in the original trace are guaranteed to also match in the predicted trace. Second, candidate races in the original trace remain viable in the predicted trace as they still refer to same location. Note that, the resolution of the virtual method call is modeled as the branch events that check the type of the target object, for which the constraints naturally guarantee the branch to take the same decision, i.e., the call to be resolved to the same method implementation.

%Finally, in a practical setting involving virtual method calls, call-site resolutions are the same across the original and predicted traces. 
%Notice that in this setting, we consider as relevant not only the targets of field dereferences but also the targets of virtual method invocations.

Formally, given pair $e$ and $e'$ of candidate racing events such that $e$ happens after $e'$ in the trace $\tau$, 
we require that
$$
\bigwedge_{ e_i \equiv {\tt y=x.f}|x.f=y \wedge e_i \in \tau|e }\
	x \equiv  \lsyn x \rsyn^{e_i}
$$
%where ${\sf env}$ is the state mapping from local variables to their value and $\sigma(t,\tau'')$ 
%(resp. $\sigma(t',\tau'')$) is the state arising at trace $t$ (resp. $t'$) immediately before event $\tau''$.
This constraint fixes that all heap dereferences  prior to the racy event retain their original base object as in the original trace $\tau$. 


By sending the above constraints to a solver, we compute the necessary schedule orders among the events as well as the mapping of the variables. The necessary schedule orders define a partial order among the events, which permit a set of schedules that define the complete order that complies with it.