src/HOL/Hoare_Parallel/document/root.tex
author wenzelm
Sun, 09 Feb 2014 17:41:17 +0100
changeset 55369 713629c2b73c
parent 32621 a073cb249a06
child 58884 be4d203d35b3
permissions -rw-r--r--
removed junk;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13106
f6561b003a35 \documentclass{report};
wenzelm
parents: 13099
diff changeset
     1
\documentclass[11pt,a4paper]{report}
13033
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
     2
\usepackage{graphicx}
13021
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
     3
\usepackage[english]{babel}
13033
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
     4
\usepackage{isabelle,isabellesym}
d6a09050a40d added session_graph;
wenzelm
parents: 13021
diff changeset
     5
\usepackage{pdfsetup}
13021
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
     6
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
     7
\urlstyle{rm}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
     8
\isabellestyle{it}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
     9
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    10
\renewcommand{\isamarkupheader}[1]{#1}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    11
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    12
\begin{document}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    13
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    14
\title{Hoare Logic for Parallel Programs}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    15
\author{Leonor Prensa Nieto}
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    16
\maketitle
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    17
13099
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    18
\begin{abstract}\noindent
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    19
  In the following theories a formalization of the Owicki-Gries and
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    20
  the rely-guarantee methods is presented. These methods are widely
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    21
  used for correctness proofs of parallel imperative programs with
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    22
  shared variables.  We define syntax, semantics and proof rules in
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    23
  Isabelle/HOL.  The proof rules also provide for programs
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    24
  parameterized in the number of parallel components. Their
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    25
  correctness w.r.t.\ the semantics is proven.  Completeness proofs
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    26
  for both methods are extended to the new case of parameterized
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    27
  programs. (These proofs have not been formalized in Isabelle. They
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    28
  can be found in~\cite{Prensa-PhD}.)  Using this formalizations we
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    29
  verify several non-trivial examples for parameterized and
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    30
  non-parameterized programs.  For the automatic generation of
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    31
  verification conditions with the Owicki-Gries method we define a
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    32
  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
    33
  verification of two garbage-collection algorithms, the second one
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    34
  parameterized in the number of mutators.
4bb592cdde0e added abstract;corrected RG_Basic Hoare rule.
prensani
parents: 13036
diff changeset
    35
19401
259e2bbba43c added references
nipkow
parents: 13106
diff changeset
    36
For excellent descriptions of this work see
259e2bbba43c added references
nipkow
parents: 13106
diff changeset
    37
\cite{NipkowP-FASE99,PrenEsp00,Prensa-PhD,Prensa-ESOP03}.
259e2bbba43c added references
nipkow
parents: 13106
diff changeset
    38
13099
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
19401
259e2bbba43c added references
nipkow
parents: 13106
diff changeset
    56
\bibliographystyle{plain}
259e2bbba43c added references
nipkow
parents: 13106
diff changeset
    57
\bibliography{root}
13021
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    58
cd0075346431 Adding root.tex for HoareParallel
prensani
parents:
diff changeset
    59
\end{document}