impl.tex

\section{Implementation}\label{sec:impl}


\subsection{Time Window and Initial Value constraints}~\label{sec:timewindow}
The trace is typically long and the constraint solver cannot scale to the whole trace. This is a known limitation to solver-based predictive analysis. Instead, we adopt the notion of time window. 
We divide the trace into $N$ traces of the same length, where $N$ is configurable parameter (1000 in our experiment). To support the time window, we need to store the values of the shared variables and local variables at the end of a window and encode such values as the inputs of the next window. 

We maintain two maps,  $sstore$ and $lstore$, for the shared variables and local variables respectively. Suppose the trace for the last window is $\tau$. The following code illustrates how we maintain the $sstore$, i.e., storing the value written by the last write with each address. Beside, the variable $e.ins.left$ represents the left hand variable inside the instruction $e.ins$.

\begin{algorithmic}[3]
\For {$a \in \mathcal{A}$}
 \State $\tau_a=W(a)$
 \State $sstore.put(a,\tau_a[|\tau_a|-1].v)$ 
\EndFor
\end{algorithmic}

%TODO define left:
\begin{algorithmic}[3]
\For {$e \in \tau$}
  \If {$e.isLocalAcc()$}
    \State $ lstore.put(e.\_def, e.v)$
  \Else
     \If{$e.isRead()$}      
        \State $ lstore.put(e.\_def, e.v)$
     \EndIf
  \EndIf 
\EndFor
\end{algorithmic}


When constructing the constraints for the next window, we specify the following constraints to encode the input values.

The following formula enhances the thread interfernce constraint to include the case that the read reads from the initial values. 

$$\Phi_{TI}=\Phi_{TI} \wedge  R=sstore.get(e_R.a) \wedge \bigvee_{e\in S} O(e_R)<O(e)$$.

The following formula encodes the input values of local variables. 

$$\Phi_{IN}=\bigvee_{l\in lstore.keys()} l=lstore.get(l)$$.
 



{\bf Optimization\ }. Before the symbolic analysis, we conduct the backward slicing by treating the racy pair as the seeds. Only those selected in the slices are preserved while the rest events are removed. 



\subsection{Scalability Issues}
Like existing predictive analyses, our approach suffers from scalability issues for two reasons. First, as we record local access events in the monitoring run,  the monitoring run takes long time, e.g., more than 2 hours, and our trace is typically large, e.g., at the GB level. To avoid the out of memory issue during the monitoring run, we store the event to the database on the fly, rather than storing them in a buffer. Besides, we terminate the monitoring run with a shutdown hook if it is beyond 30 minutes. Second,  the prediction phase needs to load the trace to memory, which easily causes out of memory problem. To solve the problem, we separate the analysis into several runs, each run restarting the JVM and resuming from the window of last run. Different runs communicate the window id using the external file. These runs are organized together automatically using the ant. The outputs of the files are merged into one summary.