\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}

% this should be the last package used
\usepackage{pdfsetup}

% urls in roman style, theory text in math-similar italics
\urlstyle{rm}
\isabellestyle{it}


\begin{document}

\title{Formalization of Conflict Analysis of Programs with Procedures, Thread Creation, and Monitors in Isabelle/HOL}
\author{Peter Lammich
        \and
        Markus M\"uller-Olm \\[2ex]
%
        Institut f\"ur Informatik, Fachbereich Mathematik und Informatik\\
        Westf\"alische Wilhelms-Universit\"at M\"unster\\[1ex]
% 
        \texttt{peter.lammich@uni-muenster.de} and \texttt{mmo@math.uni-muenster.de}
       }

% \institute{
% Institut für Informatik, Fachbereich Mathematik und Informatik\\
% Westfälische Wilhelms-Universität Münster\\
% \email{peter.lammich@uni-muenster.de} and \email{mmo@math.uni-muenster.de}
% }
\maketitle

\begin{abstract}
  In this work we formally verify the soundness and precision of a static program analysis that detects conflicts (e.g.\ data races) in programs with procedures, thread creation and monitors with the Isabelle theorem prover. 
  As common in static program analysis, our program model abstracts guarded branching by nondeterministic branching, but completely interprets the call-/return behavior of procedures, synchronization by monitors, 
  and thread creation. The analysis is based on the observation that all conflicts already occur in a class of particularly restricted schedules. These restricted schedules are suited to constraint-system-based program analysis. 

  The formalization is based upon a flowgraph-based program model with an operational semantics as reference point. 
\end{abstract}

\clearpage
\tableofcontents
\clearpage

\parindent 0pt\parskip 0.5ex

\section{Introduction}
  Conflicts are a common programming error in parallel programs. A conflict occurs if the same resource is accessed simultaneously by more than one process.
  Given a program $\pi$ and two sets of control points $U$ and $V$, the analysis problem is to decide whether there is an execution of $\pi$ that simultaneously reaches one control
  point from $U$ and one from $V$.

  In this work, we use a flowgraph-based program model that extends a previously studied model \cite{LM07} by reentrant monitors.
  In our model, programs can call recursive procedures, dynamically create new threads and synchronize 
  via reentrant monitors. As usual in static program analysis, our program model abstracts away guarded branching by nondeterministic choice. We use an operational semantics as reference point for the correctness proofs.
  It models parallel execution by interleaving, i.e. just one thread is executed at any time and context switches may occur after every step. The next step is nondeterministically selected from all threads ready for execution.
  The analysis is based on a constraint system generated from the flowgraph. From its least solution, one can decide whether control points from $U$ and $V$ are simultaneously reachable or not. 

  It is notoriously hard to analyze concurrent programs with constraint systems because of the arbitrary fine-grained interleaving.
  The key idea behind our analysis is to use a restricted scheduling: While the interleaving semantics can switch the context after each step, the restricted scheduling just allows context switches at certain points of a thread's
  execution. We can show that each conflict is also reachable under this restricted scheduling. The restricted schedules can be easily analyzed with constraint systems as most of the complexity generated by arbitrary interleaving 
  does no longer occur due to the restrictions. The remaining concurrency effects can be smoothly handled by using the concept of acquisition histories \cite{KIG05}.

  \paragraph{Related Work}
  In \cite{LM07} we present a constraint-system-based analysis for programs with thread creation and procedures but without monitors. The abstraction from synchronization is common in this line of research:
  There are automata-based techniques \cite{BMT05,EK99,EP00} as well as constraint-system-based techniques \cite{SeSt00,LM07} to analyze programs with procedures and either parallel calls or thread creation, but without any 
  synchronization. In \cite{KIG05,KG06} analysis techniques for interprocedural parallel programs with a fixed number of initial threads and nested locks are presented. These nested locks are not syntactically bound to the program 
  structure, but assumed to be well-nested, that is any unlock statement is required to release the lock that was acquired last by the thread. Moreover, there is no support for reentrant 
  locks\footnote{Reentrant locks can always be simulated by non-reentrant ones, at the cost of a worst-case exponential blowup of the program size}. 
  We use monitors instead of locks. Monitors are syntactically bound to the program structure and thus well-nestedness is guaranteed statically. Additionally we directly support reentrant monitors. Our model cannot simulate 
  well-nested locks where a lock statement and its corresponding unlock statement may be in different procedures (as in \cite{KIG05,KG06}). As common programming languages like Java also use reentrant monitors rather than locks, 
  we believe our model to be useful as well.

  \paragraph{Document structure}
  This document contains a commented formalization of these ideas as a collection of Isabelle/HOL theories. A more abstract description is in preparation.
  This document starts with formalization monitor consistent interleaving 
  (Section~\ref{thy:ConsInterleave}) and acquisition histories (Section~\ref{thy:AcquisitionHistory}). Labeled transition systems are formalized in Section~\ref{thy:LTS}, and Section~\ref{thy:ThreadTracking} defines
  the notion of interleaving semantics. Flowgraphs are defined in Section~\ref{thy:Flowgraph}, and Section~\ref{thy:Semantics} describes their operational semantics. Section~\ref{thy:Normalization} contains the formalization of
  the restricted interleaving and Section~\ref{thy:ConstraintSystems} contains the constraint systems. Finally, the main result of this development -- the correctness of the constraint systems w.r.t. to the operational semantics -- 
  is briefly stated in Section~\ref{thy:MainResult}.



%   While it is notoriously hard to analyze unrestricted interleaving semantics with constraint systems, our restricted scheduling is easy to
%   analyze

%   We use a flowgraph based program model that is an extension of the one we used in \cite{LM07}. We represent a program by an edge annotated graph. 
%   The graph is partitioned by a set of procedures, that is each node of the graph belongs to exactly
%   one procedure, and there are no edges across procedures. The nodes of the graph correspond to the control points of the program, and the edges correspond to the statements. The edges are annotated with 
%   the statements they execute. There are base statements, whose structure is not relevant for this work and thus left undefined. The further statements are call statements to call a procedure and spawn statements 
%   to create a new thread. Each procedure has a designated entry and return node as well as a set of monitors it synchronizes on, and the whole program has a designated $main$ procedure. 
%   For technical reasons, we impose some additional structural restrictions on flowgraphs. However, those restrictions do not limit the power of our analysis, as any flowgraph can be mapped to a restricted one with the same 
%   conflicts.

%   We define an operational semantics on flowgraphs. A configuration is a multiset of stacks of nodes, and a step is labelled with either the annotation of the edge that was executed or with a special return label, 
%   if a procedure return was executed. The current state of a single thread is modelled as a stack, the top entry being the node corresponding to the current control point, and the nodes deeper on the stack being stored 
%   return addresses. The thread may make any step corresponding to an outgoing edge or a return step if it is at a return node. A call step may only be performed if all monitors required by the called procedure are free. 
%   In our model, monitors are {\em reentrant}, that is a thread may recursively enter the same monitor. A spawn step may always be performed, as we constrain initial procedures of threads not to synchronize on monitors. 
%   A spawn step creates a new stack containing just the initial procedure's entry point. 
%   The concurrency aspect is modelled by interleaving, that is one step of the semantics corresponds to a single thread's step. The thread to make the next step is nondeterministically selected from all available threads that are
%   ready to make a step.

%   Based on the operational semantics, we can formally define our analysis problem. We use this definition as a reference point, that is we trust that this definition does what we want and prove our analysis does the same.
  
%   The aim of this work is to develop a constraint system based static program analysis for the simultaneous reachability problem. In the isabelle formalization, we describe the constraint systems by inductively defined sets. This
%   description is not exactly what we want, since we cannot use other lattices than the powerset lattice and cannot use finite chain height properties to derive executable algorithms. However, this description is sufficient to 
%   capture all the other aspects of the analysis. 

%   It is particular hard to describe interleaving and thread creation in a constraint system directly (c.f. \cite{BMT05}). The key idea to our algorithm is to consider a semantics that only allows for a restricted interleaving.
%   We call an execution adhering to this restricted interleaving {\em normalized}. We then show that all configurations that are reachable via some execution are also reachable via a normalized one. Thus it is sufficient to
%   consider the normalized executions, which have some nice properties allowing a concise treatment with constraint system based techniques. For the treatment of concurrency, we use the concept of 
%   {\em acquisition histories} \cite{KIG05}.
 
%   \paragraph{Related Work}
%   In \cite{LM07} we present a constraint system based analysis for programs with thread creation and procedures but without monitors. The abstraction from any synchronization is common in this line of research:
%   There are automata based techniques \cite{BMT05,EK99,EP00} as well as constraint system based techniques \cite{SeSt00,LM07} to analyze programs with procedures and either parallel calls or thread creation, but without any 
%   synchronization. In \cite{KIG05,KG06} analysis techniques for interprocedural parallel programs with a fixed number of initial threads and nested locks are developped. The nested locks are not syntactically bound to the program 
%   structure, but assumed to be well-nested, that is any unlock statement is required to be for the lock that was acquired last by the thread. Moreover, they do not support reentrant locks. We use monitors instead of locks, that are 
%   syntactically bound to the program structure and thus guarantee well-nesting. Additionally we allow reentrant locks. 
%   Our model cannot simulate the one used in \cite{KIG05,KG06} and vice versa. However, since languages like Java also use monitors rather than locks, we believe our model to also be useful.

% generated text of all theories
\input{session}

\section{Conclusion}
We have formalized a flowgraph-based model for programs with recursive procedure calls, dynamic thread creation and reentrant monitors and its operational semantics. Based on the operational semantics, we 
defined a conflict as being able to simultaneously reach two control points from two given sets $U$ and $V$ when starting at the initial program configuration, just consisting of a single thread at the
entry point of the main procedure. We then formalized a constraint-system-based analysis for conflicts and proved it sound and precise w.r.t. the operational definition of a conflict. The main idea of the analysis
was to restrict the possible schedules of a program. On the one hand, this restriction enabled the constraint system based analysis, on the other hand it did not change the set of reachable configurations (and 
thus the set of conflicts).  

We characterized the constraint systems as inductive sets. While we did not derive an executable algorithm explicitly, the steps from the inductive sets characterization to an algorithm follow the path common in program analysis
and pose no particular difficulty. The algorithm would have to construct a constraint system (system of inequalities over a finite height lattice) from a given program corresponding to the inductively defined sets studied here and 
then determine its least solution, e.g. by a worklist algorithm. In order to make the algorithm executable, we would have to introduce finiteness assumptions for our programs. The derivation of executable algorithms is 
currently in preparation.

A formal analysis of the algorithmic complexity of the problem will be presented elsewhere. Here we only present some results: Already the problem of deciding the reachability of a single control node is NP-hard, 
as can be shown by a simple reduction from SAT. On the other hand, we can decide simultaneous reachability in nondeterministic polynomial time in the program size, where the number of random bits depends on the 
possible nesting depth of the monitors. This can be shown by analyzing the constraint systems.

\paragraph{Acknowledgement} We thank Dejvuth Suwimonteerabuth for an interesting discussion about static analysis of programs with locks. We also thank the people on the Isabelle mailing list for quick and useful responses.

% optional bibliography
\bibliographystyle{abbrv}
\bibliography{root}

\end{document}

%%% Local Variables:
%%% mode: latex
%%% TeX-master: t
%%% End:
