pip: Journal/document/root.tex@2aa37de77f31 (annotated)

20 b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	1	%\documentclass{article}
b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	2	\documentclass{llncs}
b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	3	%\textwidth 130mm
b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	4	%\textheight 200mm
b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	5	%\renewenvironment{abstract}{\section*{Abstract}\small}{}
27 6b1141c5e24c cleaned up Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 24 diff changeset	6	\pagestyle{headings}
6 7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	7	\usepackage{isabelle}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	8	\usepackage{isabellesym}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	9	\usepackage{amsmath}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	10	\usepackage{amssymb}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	11	\usepackage{mathpartir}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	12	\usepackage{tikz}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	13	\usepackage{pgf}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	14	\usepackage{pdfsetup}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	15	\usepackage{ot1patch}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	16	\usepackage{times}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	17	\usepackage{stmaryrd}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	18	\usepackage{url}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	19	\usepackage{color}
7 0514be2ad83e started code explanation Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	20	\usepackage{courier}
32 e861aff29655 made some modifications. Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 27 diff changeset	21	\usetikzlibrary{patterns}
7 0514be2ad83e started code explanation Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	22	\usepackage{listings}
0514be2ad83e started code explanation Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	23	\lstset{language=C,
0514be2ad83e started code explanation Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	24	numbers=left,
0514be2ad83e started code explanation Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	25	basicstyle=\small\ttfamily,
0514be2ad83e started code explanation Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	26	numberstyle=\footnotesize, frame=tb}
6 7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	27
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	28	\urlstyle{rm}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	29	\isabellestyle{it}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	30	\renewcommand{\isastyleminor}{\it}%
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	31	\renewcommand{\isastyle}{\normalsize\it}%
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	32
7 0514be2ad83e started code explanation Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 6 diff changeset	33	%%%\titlerunning{Proving the Priority Inheritance Protocol Correct}
6 7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	34	\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	35	\renewcommand{\isasymequiv}{$\dn$}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	36	\renewcommand{\isasymemptyset}{$\varnothing$}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	37	\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	38	\renewcommand{\isasymiota}{}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	39
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	40	\newcommand{\numbered}[1]{\refstepcounter{equation}{\rm(\arabic{equation})}\label{#1}}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	41	\definecolor{mygrey}{rgb}{.80,.80,.80}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	42
20 b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	43	%\newtheorem{definition}{Definition}
b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	44	%\newtheorem{theorem}[definition]{Theorem}
b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	45	%\newtheorem{lemma}[definition]{Lemma}
b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	46	%\newtheorem{proof}{Proof}
b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	47	%\renewcommand{\theproof}{}
b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	48	%\newcommand{\qed}{\hfill \mbox{\raggedright \rule{0.1in}{0.1in}}}
6 7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	49
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	50
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	51	\begin{document}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	52	\renewcommand{\thefootnote}{$\star$}
32 e861aff29655 made some modifications. Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 27 diff changeset	53	\footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.
e861aff29655 made some modifications. Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 27 diff changeset	54	Compared with that paper we give an actual implementation of our formalised scheduling
e861aff29655 made some modifications. Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 27 diff changeset	55	algorithm in C and the operating system PINTOS. Our implementation follows closely all results
75 2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	56	we proved about optimisations of the Priority Inheritance Protocol. We are giving in this paper
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	57	more details about the proof and also surveying
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	58	the existing literature in more depth.}
6 7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	59	\renewcommand{\thefootnote}{\arabic{footnote}}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	60
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	61	\title{Priority Inheritance Protocol Proved Correct}
20 b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	62	\author{Xingyuan Zhang$^1$, Christian Urban$^2$ and Chunhan Wu$^1$}
b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	63	\institute{PLA University of Science and Technology, China \and
b56616fd88dd added Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 17 diff changeset	64	King's College London, United Kingdom}
6 7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	65	\maketitle
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	66
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	67	\begin{abstract}
75 2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	68	In real-time systems with threads, resource locking and priority
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	69	sched\-uling, one faces the problem of Priority Inversion. This
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	70	problem can make the behaviour of threads unpredictable and the
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	71	resulting bugs can be hard to find. The Priority Inheritance Protocol
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	72	is one solution implemented in many systems for solving this problem,
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	73	but the correctness of this solution has never been formally verified
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	74	in a theorem prover. As already pointed out in the literature, the
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	75	original informal investigation of the Property Inheritance Protocol
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	76	presents a correctness ``proof'' for an \emph{incorrect} algorithm. In
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	77	this paper we fix the problem of this proof by making all notions
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	78	precise and implementing a variant of a solution proposed earlier. We
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	79	also generalise the scheduling problem to the practically relevant case where
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	80	critical sections can overlap. Our formalisation in Isabelle/HOL not
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	81	just uncovers facts not mentioned in the literature, but also helps
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	82	with implementing efficiently this protocol. Earlier correct
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	83	implementations were criticised as too inefficient. Our formalisation
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	84	is based on Paulson's inductive approach to verifying protocols; our
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	85	implementation builds on top of the small PINTOS operating system used
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	86	for teaching.\medskip
6 7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	87
75 2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	88	{\bf Keywords:} Priority Inheritance Protocol, formal correctness proof,
2aa37de77f31 updated paper Christian Urban <christian dot urban at kcl dot ac dot uk> parents: 35 diff changeset	89	real-time systems, Isabelle/HOL
6 7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	90	\end{abstract}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	91
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	92	\input{session}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	93
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	94	%\bibliographystyle{plain}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	95	%\bibliography{root}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	96
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	97	\end{document}
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	98
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	99	%%% Local Variables:
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	100	%%% mode: latex
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	101	%%% TeX-master: t
7f2493296c39 updated Christian Urban <christian dot urban at kcl dot ac dot uk> parents: diff changeset	102	%%% End:

author	Christian Urban <christian dot urban at kcl dot ac dot uk>
	Thu, 14 Jan 2016 03:29:22 +0000
changeset 75	2aa37de77f31
parent 35	92f61f6a0fe7
child 142	10c16b85a839
permissions	-rwxr-xr-x