src/HOL/HoareParallel/document/root.tex
author wenzelm
Tue, 07 May 2002 14:27:07 +0200
changeset 13106 f6561b003a35
parent 13099 4bb592cdde0e
child 19401 259e2bbba43c
permissions -rw-r--r--
\documentclass{report};
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13033
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
     1
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
     2
% $Id$
13021
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
     3
13106
f6561b003a35 \documentclass{report};
wenzelm
parents: 13099
diff changeset
     4
\documentclass[11pt,a4paper]{report}
13033
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
     5
\usepackage{graphicx}
13021
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
     6
\usepackage[english]{babel}
13033
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
     7
\usepackage{isabelle,isabellesym}
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
     8
\usepackage{pdfsetup}
13021
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
     9
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    10
\urlstyle{rm}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    11
\isabellestyle{it}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    12
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    13
\renewcommand{\isamarkupheader}[1]{#1}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    14
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    15
\begin{document}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    16
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    17
\title{Hoare Logic for Parallel Programs}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    18
\author{Leonor Prensa Nieto}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    19
\maketitle
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    20
13099
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    21
\begin{abstract}\noindent
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    22
  In the following theories a formalization of the Owicki-Gries and
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    23
  the rely-guarantee methods is presented. These methods are widely
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    24
  used for correctness proofs of parallel imperative programs with
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    25
  shared variables.  We define syntax, semantics and proof rules in
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    26
  Isabelle/HOL.  The proof rules also provide for programs
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    27
  parameterized in the number of parallel components. Their
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    28
  correctness w.r.t.\ the semantics is proven.  Completeness proofs
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    29
  for both methods are extended to the new case of parameterized
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    30
  programs. (These proofs have not been formalized in Isabelle. They
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    31
  can be found in~\cite{Prensa-PhD}.)  Using this formalizations we
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    32
  verify several non-trivial examples for parameterized and
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    33
  non-parameterized programs.  For the automatic generation of
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    34
  verification conditions with the Owicki-Gries method we define a
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    35
  tactic based on the proof rules.  The most involved examples are the
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    36
  verification of two garbage-collection algorithms, the second one
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    37
  parameterized in the number of mutators.
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    38
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    39
\end{abstract}
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    40
13021
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    41
\pagestyle{plain}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    42
\thispagestyle{empty}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    43
\tableofcontents
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    44
13036
wenzelm
parents: 13033
diff changeset
    45
\clearpage
wenzelm
parents: 13033
diff changeset
    46
13033
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
    47
\begin{center}
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
    48
  \includegraphics[scale=0.7]{session_graph}  
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
    49
\end{center}
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
    50
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
    51
\newpage
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
    52
13021
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    53
\parindent 0pt\parskip 0.5ex
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    54
\input{session}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    55
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    56
%\bibliographystyle{plain}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    57
%\bibliography{root}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    58
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    59
\end{document}