Commit edb142a1 authored by Marek Chalupa's avatar Marek Chalupa
Browse files

update concur 18

parent dd401f39

concur18_spring/main.tex

+410 −32
Original line number Diff line number Diff line 
\documentclass[sans]{beamer}

\usetheme{metropolis}



\usepackage[linesnumbered,ruled,vlined]{algorithm2e} 

\usepackage{lmodern}

\usepackage{tikz}

\usepackage{pdfpages}
@@ -89,7 +90,47 @@ 


%% -------------------------------------------------------------------

\begin{frame}[fragile]

\frametitle{Stateful (explicit) model checking}

\frametitle{Model Checking of Parallel Programs}



\begin{columns}

\hspace*{1.5mm}

\begin{column}{0.3\textwidth}

\vspace*{-2mm}

\begin{lstlisting}

x = 0;



thread1() {

  x = 1;

  assert(x == 1);

}



thread2() {

  x = 2;

  assert(x == 2);

}

\end{lstlisting}

\end{column}



\begin{column}{0.6\textwidth}

{\bf Visible instruction} is an instruction that modifes the global state. \\[1em]

\pause

{\bf Event} is a sequence of consecutive non-visible instructions from

one process ending with a visible instruction. \\[1em]

\pause

{\bf Conflicting Events} are two events s.t. they modify

the same memory and at~least one of the events is write.\\[1em]



\pause

{\bf Trace} is a sequence of events.

\end{column}

\end{columns}



\end{frame}

%% -------------------------------------------------------------------



%% -------------------------------------------------------------------

\begin{frame}[fragile]

\frametitle{Stateful model checking}



\begin{tabular}{c p{2cm} c}
@@ -108,7 +149,7 @@ thread2() { 
\end{lstlisting}

\pause

&&

\begin{tikzpicture}[overlay, xshift=1.7cm, yshift=3cm]

\begin{tikzpicture}[overlay, xshift=1.5cm, yshift=3cm]

  \tikzset{

    state/.style={draw, minimum width=1cm},

    event1/.style={draw,circle, fill=red!20},
@@ -122,18 +163,17 @@ thread2() { 
\node[state] (s4) at(-2, -3) { \small x = 1 };

\node[state] (s5) at (-.5, -3) { \small x = 2 };

\node[state] (s6) at (2.5, -3) { \small x = 2 };

\node[state] (s7) at (1.2, -3.5) { \small x = 1 };

\node[state] (s7) at (1, -3.5) { \small x = 1 };



\node[state] (s8) at (-2, -4.5) { \small x = 2 };

\node[state] (s9) at (-2, -6) { \small x = 2 };



\node[state] (s10) at(-.5, -5) { \small x = 2 };

\node[state] (s10) at(-.5, -5.3) { \small x = 2 };



\node[state] (e) at(1.5, -6) { \small \color{red}{err} };

\node[state] (e) at(1, -6.5) { \small \color{red}{err} };



\node[] (d1) at(2.5, -4.5) { ... };



%\node[state] (error) at (0, -2){ \tiny ERR };

\node[state] (s11) at(2.5, -4.5) { \small x = 1 };

\node[state] (s12) at(2.5, -6) { \small x = 1 };



\draw[->] (s1) edge node[event1]{\tiny $1$} (s2);

\draw[->] (s1) edge node[event2]{\tiny $1$}(s3);
@@ -144,8 +184,9 @@ thread2() { 
\draw[->] (s4) edge node[event2]{\tiny $1$}(s8);

\draw[->] (s8) edge node[event2]{\tiny $2$}(s9);



\draw[->] (s6) edge node[event1]{\tiny $1$}(d1);

\draw[->] (s5) edge node[event2]{\tiny $2$}(s10);

\draw[->] (s6) edge node[event1]{\tiny $1$}(s11);

\draw[->] (s11) edge node[event1]{\tiny $2$}(s12);



\draw[->] (s7) edge node[event2]{\tiny $2$}(e);

\draw[->] (s10) edge node[event1]{\tiny $2$}(e);
@@ -173,6 +214,73 @@ thread2() { 
\end{frame}

	%% -------------------------------------------------------------------



%%% -------------------------------------------------------------------

%\begin{frame}[fragile]

%\frametitle{Partial Order Reduction}



%\begin{columns}

%\begin{column}{0.4\textwidth}

%\centering

%Independent events\\[1em]

%\begin{tikzpicture}

%  \tikzset{

%    event1/.style={draw,circle, fill=red!20},

%    event2/.style={draw,circle, fill=blue!20},

%  }



%  \node[circle, draw] (s1) at(-1.5, 0){};

%  \node[circle, draw] (s2) at(0,  1.5) {};

%  \node[circle, draw] (s3) at(0, -1.5) {};

%  \node[circle, draw] (s4) at(1.5,0) {};



%  \draw[->] (s1) edge node[event1]{2} (s2);

%  \draw[->] (s1) edge node[event2]{2} (s3);



%  \draw[->] (s2) edge node[event2]{2} (s4);

%  \draw[->] (s3) edge node[event1]{2} (s4);



%\end{tikzpicture}

%\end{column}

%\begin{column}{0.6\textwidth}

%\pause

%{\bf Mazurkiewitcz equivalence}:\\

% Two traces are equivalent iff one can be obtained from the other by swapping

% two adjacent independent events.

%\end{column}

%\end{columns}



%\end{frame}

%%% -------------------------------------------------------------------



%%% -------------------------------------------------------------------

\begin{frame}[fragile]

\frametitle{Partial Order Reduction}



\begin{center}

Independent events\\[1em]

\begin{tikzpicture}

  \tikzset{

    event1/.style={draw,circle, fill=red!20},

    event2/.style={draw,circle, fill=blue!20},

  }



  \node[circle, draw] (s1) at(-1.5, 0){};

  \node[circle, draw] (s2) at(0,  1.5) {};

  \node[circle, draw] (s3) at(0, -1.5) {};

  \node[circle, draw] (s4) at(1.5,0) {};



  \draw[->] (s1) edge node[event1]{2} (s2);

  \draw[->] (s1) edge node[event2]{2} (s3);



  \draw[->] (s2) edge node[event2]{2} (s4);

  \draw[->] (s3) edge node[event1]{2} (s4);



\end{tikzpicture}

\end{center}

\end{frame}

%%% -------------------------------------------------------------------





%% -------------------------------------------------------------------

\begin{frame}[fragile]

\frametitle{Stateless model checking}
@@ -193,7 +301,7 @@ thread2() { 
}

\end{lstlisting}

&&

\begin{tikzpicture}[overlay, xshift=1.7cm, yshift=3cm]

\begin{tikzpicture}[overlay, xshift=1.5cm, yshift=3cm]

  \tikzset{

    state/.style={draw, circle},

    event1/.style={draw,circle, fill=red!20},
@@ -207,18 +315,20 @@ thread2() { 
\node[state] (s4) at(-2, -3) {};

\node[state] (s5) at (-.7, -3) { };

\node[state] (s6) at (2.5, -3) { };

\node[state] (s7) at (1.2, -3.5) {};

\node[state] (s7) at (1, -3.5) {};



\node[state] (s8) at (-2, -4.5) {};

\node[state] (s9) at (-2, -6) {};



\node[state] (s10) at(-.7, -5) {};



\node[state] (s11) at(2.5, -4.5) {};

\node[state] (s12) at(2.5, -6) {};



\node[state, rectangle] (e1) at(0.3, -4) { \color{red}{err}};

\node[state, rectangle] (e2) at(-.5, -6.5) { \color{red}{err}};

\node[state, rectangle] (e3) at(1.5, -6) { \color{red}{err}};

\node[state, rectangle] (e2) at(-.7, -6.5) { \color{red}{err}};

\node[state, rectangle] (e3) at(1, -6) { \color{red}{err}};



\node[] (d1) at(2.5, -4.5) { ... };



\draw[->] (s1) edge node[event1]{\tiny $1$} (s2);

\draw[->] (s1) edge node[event2]{\tiny $1$}(s3);
@@ -229,8 +339,9 @@ thread2() { 
\draw[->] (s4) edge node[event2]{\tiny $1$}(s8);

\draw[->] (s8) edge node[event2]{\tiny $2$}(s9);



\draw[->] (s6) edge node[event1]{\tiny $1$}(d1);

\draw[->] (s5) edge node[event2]{\tiny $2$}(s10);

\draw[->] (s6) edge node[event1]{\tiny $1$}(s11);

\draw[->] (s11) edge node[event1]{\tiny $2$}(s12);



\draw[->] (s7) edge node[event2]{\tiny $2$}(e3);

\draw[->] (s10) edge node[event1]{\tiny $2$}(e2);
@@ -258,7 +369,6 @@ thread2() { 
\end{frame}

	%% -------------------------------------------------------------------





	%% -------------------------------------------------------------------

\begin{frame}[fragile]

\frametitle{Dynamic Partial Order Reduction}
@@ -367,21 +477,290 @@ thread2() { 
	%% -------------------------------------------------------------------





\section{Data-Centric DPOR}



	%% -------------------------------------------------------------------

\begin{frame}[fragile]

\frametitle{Motivation}



\begin{tabular}{c p{2cm} c}



\begin{lstlisting}

x = 0;



thread1() {

  x = 1;

  assert(x == 1);

}



thread2() {

  x = 2;

  assert(x == 2);

}

\end{lstlisting}

&&



\begin{tikzpicture}[overlay, yshift=-1.5cm]

  \tikzset{

    event1/.style={draw,circle, fill=red!20},

    event2/.style={draw,circle, fill=blue!20},

  }



  \node[event1] (nd11) at (0,0) {\tiny $1$};

  \node[event1] (nd12) at (1,0) {\tiny $2$};

  \node[event2] (nd13) at (2,0) {\tiny $1$};

  \node[event2] (nd14) at (3,0) {\tiny $2$};





  \node[event2] (nd21) at (0,1) {\tiny $1$};

  \node[event2] (nd22) at (1,1) {\tiny $2$};

  \node[event1] (nd23) at (2,1) {\tiny $1$};

  \node[event1] (nd24) at (3,1) {\tiny $2$};



  \node[event1] (nd31) at (0,2) {\tiny $1$};

  \node[event2] (nd32) at (1,2) {\tiny $1$};

  \node[event1] (nd33) at (2,2) {\tiny $2$};

  \node[event2] (nd34) at (3,2) {\tiny $2$};



  \node[event2] (nd41) at (0,3) {\tiny $1$};

  \node[event1] (nd42) at (1,3) {\tiny $1$};

  \node[event1] (nd43) at (2,3) {\tiny $2$};

  \node[event2] (nd44) at (3,3) {\tiny $2$};



  \draw (nd11) -- (nd12) -- (nd13) -- (nd14);

  \draw (nd21) -- (nd22) -- (nd23) -- (nd24);

  \draw (nd31) -- (nd32) -- (nd33) -- (nd34);

  \draw (nd41) -- (nd42) -- (nd43) -- (nd44);



\pause

  \node[overlay, draw, dashed, minimum width=4cm, minimum height=1.8cm] at (1.5,0.5){};



\end{tikzpicture}



\end{tabular}



\begin{tikzpicture}[overlay]

  \tikzset{

    event1/.style={draw,circle, fill=red!20},

    event2/.style={draw,circle, fill=blue!20},

  }



  \node[event1,overlay]  at (-0.3,4.38){\tiny $1$};

  \node[event1,overlay]  at (-0.3,3.78) {\tiny $2$};



  \node[event2,overlay]  at (-0.3,1.63){\tiny $1$};

  \node[event2,overlay]  at (-0.3,1.03) {\tiny $2$};

\end{tikzpicture}





\end{frame}

	%% -------------------------------------------------------------------





\section{Data-Centric DPOR}

%% -------------------------------------------------------------------

\begin{frame}

	\frametitle{Combination -- Challenges}

\frametitle{Observation Function}

For a trace $t$, be $<_t$ the total order of events in $t$.

Further, denote $W(t)$ the write events from $t$, $R(t)$ the read events

from $t$ and $Confl(e_1, e_2)$ the predicate that $e_1$ and $e_2$ are conflicting.\\[2em]



\pause



Given a trace $t$, we define the {\bf observation function} of the trace~$t$,

$O_t : R(t) \rightarrow W(t)$, such that $O_t(r) = w$ iff

\begin{itemize}

		\item How to decompose the program?

		\item What technique use for which program fragment?

		\item How to apply and refine abstraction?

		\item How to analyze fragments on-demand?

		\item How to efficiently  parallelize computation?

		\item Parallel programs?

	\item[(1)]  $w <_t r$

	\item[(2)]  $\forall w' \in W(t): Confl(r, w') \implies (w' <_t w) \lor (w' >_t r)$

\end{itemize}

\vspace{1.3em}



\pause



{\bf Observation equivalence}: we say that traces $t_1$ and $t_2$ are equivalent

iff $O_{t_1}$ = $O_{t_2}$.



\end{frame}

%% -------------------------------------------------------------------



	%% -------------------------------------------------------------------

\begin{frame}[fragile]

\frametitle{Observation Equivalence}



\begin{tabular}{c p{2cm} c}



\begin{lstlisting}

x = 0;



thread1() {

  x = 1;

  assert(x == 1);

}



thread2() {

  x = 2;

  assert(x == 2);

}

\end{lstlisting}

&&



\begin{tikzpicture}[overlay, yshift=-1.5cm]

  \tikzset{

    event1/.style={draw,circle, fill=red!20},

    event2/.style={draw,circle, fill=blue!20},

  }



  \node[event1] (nd11) at (0,0) {\tiny $1$};

  \node[event1] (nd12) at (1,0) {\tiny $2$};

  \node[event2] (nd13) at (2,0) {\tiny $1$};

  \node[event2] (nd14) at (3,0) {\tiny $2$};





  \node[event2] (nd21) at (0,1) {\tiny $1$};

  \node[event2] (nd22) at (1,1) {\tiny $2$};

  \node[event1] (nd23) at (2,1) {\tiny $1$};

  \node[event1] (nd24) at (3,1) {\tiny $2$};



  \node[event1] (nd31) at (0,2) {\tiny $1$};

  \node[event2] (nd32) at (1,2) {\tiny $1$};

  \node[event1] (nd33) at (2,2) {\tiny $2$};

  \node[event2] (nd34) at (3,2) {\tiny $2$};



  \node[event2] (nd41) at (0,3) {\tiny $1$};

  \node[event1] (nd42) at (1,3) {\tiny $1$};

  \node[event1] (nd43) at (2,3) {\tiny $2$};

  \node[event2] (nd44) at (3,3) {\tiny $2$};



  \draw (nd11) -- (nd12) -- (nd13) -- (nd14);

  \draw (nd21) -- (nd22) -- (nd23) -- (nd24);

  \draw (nd31) -- (nd32) -- (nd33) -- (nd34);

  \draw (nd41) -- (nd42) -- (nd43) -- (nd44);



  \node[overlay, draw, dashed, minimum width=4cm, minimum height=1.8cm] at (1.5,0.5){};

  \node[overlay, draw, dashed, minimum width=4cm, minimum height=.9cm] at (1.5,2){};

  \node[overlay, draw, dashed, minimum width=4cm, minimum height=.9cm] at (1.5,3){};



\end{tikzpicture}



\end{tabular}



\begin{tikzpicture}[overlay]

  \tikzset{

    event1/.style={draw,circle, fill=red!20},

    event2/.style={draw,circle, fill=blue!20},

  }



  \node[event1,overlay]  at (-0.3,4.38){\tiny $1$};

  \node[event1,overlay]  at (-0.3,3.78) {\tiny $2$};



  \node[event2,overlay]  at (-0.3,1.63){\tiny $1$};

  \node[event2,overlay]  at (-0.3,1.03) {\tiny $2$};

\end{tikzpicture}





\end{frame}

	%% -------------------------------------------------------------------







%% -------------------------------------------------------------------

\begin{frame}

\frametitle{Annotations}

Let $W$ ($R$) be the set of write (read, resp.) events.

An~{\bf Annotation pair} $(A^+, A^-)$ is a pair of partial functions

\begin{itemize}

	\item (1) $A^+: R \rightarrow W$ called {\it possitive annotation}

	\item (2) $A^-: R \rightarrow 2^W$ called {\it negative annotation}

\end{itemize}

\vspace{1em}



A positive annotation $A^+$ is {\bf realizable} iff there exists a trace $t$,

s.t. $O_t$ = $A_+$.

\end{frame}

%% -------------------------------------------------------------------



%% -------------------------------------------------------------------

\begin{frame}[fragile]

\frametitle{The Algorithm}



\begin{algorithm}[H]

  \SetKwInOut{Input}{Inputs}

  \Input{A maximal trace $t$ and annotation pair $(A^+, A^-)$}



  \ForEach{read $r \in t$ in increasing order by $<_t$, $r \not \in Dom(A^+)$}{

    %\Comment{Find conflicting writes allowed by $A^-$}}

    \ForEach{$w \in t$ s.t. $Confl(r,w)$ and $w \not \in A^-(r)$} {

			$A^+_{r,w} \gets A^+ \cup \{(r,w)\}$



			Let $t' \gets Realize(A^+_{r,w}$)



			\If {$t' \neq \bot$} {

				$t'' \gets ${maximal extension of t'}



				$A^-(r) \gets A^-(r) \cup \{w\}$



				$A_{r,w}  \gets  (A^+_{r,w}, A^-)$



				DC-DPOR(t'', $(A^+_{r,w}, A^-)$)

			}

		}

  }

\caption{DC-DPOR Algorithm}

\end{algorithm}



\end{frame}

%% ------------------------------------------------------------------

\section{Realizing Annotations}



%% -------------------------------------------------------------------

\begin{frame}

\frametitle{Communication Graph}

{\bf Communication graph} is an undirected graph G = (P, E) where P

is the set of processes (threads) and $E \subseteq P \times P$ is a

set of edges s.t.:\\[.5cm]

$(p_1, p_2) \in E$ iff $p_1$ and $p_2$ access the same shared resource.

\end{frame}

%% -------------------------------------------------------------------







%% -------------------------------------------------------------------

\begin{frame}

\frametitle{Realizing Annotations}

\begin{itemize}

	\item Depends on communication graph.

\end{itemize}

\end{frame}

%% -------------------------------------------------------------------



%% -------------------------------------------------------------------

\begin{frame}

\frametitle{Acyclic Communication Graphs}

\begin{itemize}

	\item Depends on communication graph.

\end{itemize}



\end{frame}

%% -------------------------------------------------------------------



%% -------------------------------------------------------------------

\begin{frame}

\frametitle{Cyclic Communication Graphs}

\begin{itemize}

	\item Depends on communication graph.

\end{itemize}



\end{frame}

%% -------------------------------------------------------------------







%% -------------------------------------------------------------------

\begin{frame}

\frametitle{Conclusions}

\begin{itemize}

	\item Alg. based on more coarse

	\item Exponential succintness

  \item Polynomial alg. for acyclic

\end{itemize}

\pause

\vspace*{1cm}
@@ -389,5 +768,4 @@ thread2() { 
\end{frame}

%% -------------------------------------------------------------------





\end{document}

paradise17_autumn/sources/symbiotic.txt

+1 −1
Original line number Diff line number Diff line 
 ~/src/symbiotic-dbg/install/bin/symbiotic --prp=memsafety --debug=slicer --pta=fs ~/src/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i
 
 ~/src/symbiotic-dbg/install/bin/symbiotic --prp=memsafety --debug=slicer --pta=fi ~/src/sv-benchmarks/c/busybox-1.22.0/chgrp-incomplete_true-no-overflow_false-valid-memtrack.i