--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Journal/document/root.tex	Mon Dec 17 12:34:24 2012 +0000
@@ -0,0 +1,94 @@
+\documentclass{article}
+\textwidth 130mm
+\textheight 200mm
+\renewenvironment{abstract}{\section*{Abstract}\small}{}
+\usepackage{isabelle}
+\usepackage{isabellesym}
+\usepackage{amsmath}
+\usepackage{amssymb}
+\usepackage{mathpartir}
+\usepackage{tikz}
+\usepackage{pgf}
+%\usetikzlibrary{arrows,automata,decorations,fit,calc}
+%\usetikzlibrary{shapes,shapes.arrows,snakes,positioning}
+%\usepgflibrary{shapes.misc} % LATEX and plain TEX and pure pgf
+%\usetikzlibrary{matrix}
+\usepackage{pdfsetup}
+\usepackage{ot1patch}
+\usepackage{times}
+%%\usepackage{proof}
+%%\usepackage{mathabx}
+\usepackage{stmaryrd}
+\usepackage{url}
+\usepackage{color}
+%%%\titlerunning{Proving the Priority Inheritance Protocol Correct}
+
+
+\urlstyle{rm}
+\isabellestyle{it}
+\renewcommand{\isastyleminor}{\it}%
+\renewcommand{\isastyle}{\normalsize\it}%
+
+
+\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
+\renewcommand{\isasymequiv}{$\dn$}
+\renewcommand{\isasymemptyset}{$\varnothing$}
+\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
+\renewcommand{\isasymiota}{}
+
+\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
+\definecolor{mygrey}{rgb}{.80,.80,.80}
+
+\newtheorem{definition}{Definition}
+\newtheorem{theorem}[definition]{Theorem}
+\newtheorem{lemma}[definition]{Lemma}
+\newtheorem{proof}{Proof}
+\renewcommand{\theproof}{}
+\newcommand{\qed}{\hfill \mbox{\raggedright \rule{0.1in}{0.1in}}}
+
+
+\begin{document}
+\renewcommand{\thefootnote}{$\star$}
+\footnotetext[1]{This is a revised and expanded version of \cite{ZhangUrbanWu12}.}
+\renewcommand{\thefootnote}{\arabic{footnote}}
+
+\title{Priority Inheritance Protocol Proved Correct}
+\author{Xingyuan Zhang, Christian Urban and Chunhan Wu}
+%\institute{PLA University of Science and Technology, China \and 
+%           King's College London, United Kingdom}
+\maketitle
+
+\begin{abstract}
+In real-time systems with threads, resource locking and 
+priority sched\-uling, one faces the problem of Priority
+Inversion. This problem can make the behaviour of threads
+unpredictable and the resulting bugs can be hard to find.  The
+Priority Inheritance Protocol is one solution implemented in many
+systems for solving this problem, but the correctness of this solution
+has never been formally verified in a theorem prover. As already
+pointed out in the literature, the original informal investigation of
+the Property Inheritance Protocol presents a correctness ``proof'' for
+an \emph{incorrect} algorithm. In this paper we fix the problem of
+this proof by making all notions precise and implementing a variant of
+a solution proposed earlier. Our formalisation in Isabelle/HOL
+uncovers facts not mentioned in the literature, but also shows how to
+efficiently implement this protocol. Earlier correct implementations
+were criticised as too inefficient. Our formalisation is based on
+Paulson's inductive approach to verifying protocols; our implementation
+is on top of the small PINTOS operating system.\medskip
+
+%{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof, 
+%real-time systems, Isabelle/HOL
+\end{abstract}
+
+\input{session}
+
+%\bibliographystyle{plain}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End: