\RequirePackage{luatex85}

\documentclass[11pt]{llncs}
\usepackage[T1]{fontenc}
\pdfoutput=1
\usepackage{geometry}
\geometry{
  a4paper,         % or letterpaper
  textwidth=15cm,  % llncs has 12.2cm
  textheight=24cm, % llncs has 19.3cm
  heightrounded,   % integer number of lines
  hratio=1:1,      % horizontally centered
  vratio=2:3,      % not vertically centered
}

\usepackage{amsmath}

\usepackage{graphicx}
\usepackage{mathpartir}
\usepackage{float}

\usepackage{cite}
% produce nice graphics using tikz and pgf
%\usepackage{tikz}
%\usetikzlibrary{snakes}

\usepackage{xspace}
\newcommand{\cf}{cf.\@\xspace}
\newcommand{\eg}{e.g.,\xspace}
\newcommand{\ie}{i.e.,\xspace}
\newcommand{\Sound}{sound}
\usepackage{isabelle,isabellesym}

\usepackage{amssymb}

% We redefine it use the ragged2e package for \RaggedRight which makes better
% use of hyphenation in Latex2e compared to standard \raggedright
\usepackage{ragged2e}
% {tabularx} provides an expanding column specifier X
\usepackage{tabularx} % todo not loading tabularx seems to break compilation
\usepackage{booktabs}

\usepackage{longtable}

\usepackage{amsmath}
\usepackage{stmaryrd}
\usepackage{subfig}

\usepackage[draft]{fixme}
% provides {inparaenum} for enumerations inside a paragraph
\usepackage[defblank]{paralist}
% make roman numerals default for {inparaenum}:
\let\oldinparaenum=\inparaenum
\def\inparaenum{\oldinparaenum[(i)]}

%inference rules
\usepackage{mathpartir}

%for greek letters in our Isabelle setup
\usepackage[greek, english]{babel}
\usepackage{type1cm}

\usepackage{float}
\usepackage{tikz}
\usetikzlibrary{calc}

\usepackage{pdfsetup}

%fix robustness issue in Isabelle 2007
\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}

\newcommand{\isabellestylesf}{%
\isabellestyleit%
\renewcommand{\isastyle}{\small\sf}%
\renewcommand{\isastyleminor}{\sf}%
\renewcommand{\isastylescript}{\scriptsize}%
\renewcommand{\isascriptstyle}{\def\isamath####1{####1}\def\isatext####1{\mbox{\isastylescript####1}}\def\isagreek####1{\foreignlanguage{greek}{\mbox{\isastylescript####1}}}}%
\renewcommand{\isacharprime}{\ensuremath{\mskip2mu{'}\mskip-2mu}}%

\DeclareRobustCommand{\isactrlsub}[1]{{\isascriptstyle${}\mathsf{\sb{\vphantom{gb}##1}}$}}%
\DeclareRobustCommand{\isactrlsup}[1]{{\isascriptstyle${}\mathsf{\sp{\vphantom{gb}##1}}$}}%
\DeclareRobustCommand{\isactrlisub}[1]{{\isascriptstyle${}\mathsf{\sb{\vphantom{gb}##1}}$}}%
\DeclareRobustCommand{\isactrlisup}[1]{{\isascriptstyle${}\mathsf{\sp{\vphantom{gb}##1}}$}}%
\DeclareRobustCommand{\isactrlbsub}{\bgroup\isascriptstyle\begin{math}{}\mathsf\bgroup\sb\bgroup}%
\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\end{math}\egroup}%
\DeclareRobustCommand{\isactrlbsup}{\bgroup\isascriptstyle\begin{math}{}\mathsf\bgroup\sp\bgroup}%
\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\end{math}\egroup}%

\renewcommand{\isamarkupchapter}[1]{\isastyletext\chapter{##1}}
\renewcommand{\isamarkupsection}[1]{\isastyletext\section{##1}}
\renewcommand{\isamarkupsubsection}[1]{\isastyletext\subsection{##1}}
\renewcommand{\isamarkupsubsubsection}[1]{\isastyletext\subsubsection{##1}}
%\renewcommand{\isamarkupsect}[1]{\isastyletext\section{##1}}
%\renewcommand{\isamarkupsubsect}[1]{\isastyletext\subsection{##1}}
%\renewcommand{\isamarkupsubsubsect}[1]{\isastyletext\subsubsection{##1}}

%we use babel for greek letters to easily obtain different fontshapes; \mbox helps in math mode
\newcommand{\isagreek}[1]{\foreignlanguage{greek}{\mbox{##1}}}
\renewcommand{\isasymalpha}{\isagreek{a}}
\renewcommand{\isasymbeta}{\isagreek{b}}
\renewcommand{\isasymgamma}{\isagreek{g}}
\renewcommand{\isasymdelta}{\isagreek{d}}
\renewcommand{\isasymepsilon}{\isagreek{e}}
\renewcommand{\isasymzeta}{\isagreek{z}}
\renewcommand{\isasymeta}{\isagreek{h}}
\renewcommand{\isasymtheta}{\isagreek{j}}
\renewcommand{\isasymiota}{\isagreek{i}}
\renewcommand{\isasymkappa}{\isagreek{k}}
\renewcommand{\isasymlambda}{\isamath{\lambda}}
\renewcommand{\isasymmu}{\isagreek{m}}
\renewcommand{\isasymnu}{\isagreek{n}}
\renewcommand{\isasymxi}{\isagreek{x}}
\renewcommand{\isasympi}{\isagreek{p}}
\renewcommand{\isasymrho}{\isagreek{r}}
\renewcommand{\isasymsigma}{\isagreek{sv}}
\renewcommand{\isasymtau}{\isagreek{t}}
\renewcommand{\isasymupsilon}{\isagreek{u}}
\renewcommand{\isasymphi}{\isagreek{f}}
\renewcommand{\isasymchi}{\isagreek{q}}
\renewcommand{\isasympsi}{\isagreek{y}}
\renewcommand{\isasymomega}{\isagreek{w}}
\renewcommand{\isasymGamma}{\isagreek{G}}
\renewcommand{\isasymDelta}{\isagreek{D}}
\renewcommand{\isasymTheta}{\isagreek{J}}
\renewcommand{\isasymLambda}{\isagreek{L}}
\renewcommand{\isasymXi}{\isagreek{X}}
\renewcommand{\isasymPi}{\isagreek{P}}
\renewcommand{\isasymSigma}{\isagreek{Sv}}
\renewcommand{\isasymUpsilon}{\isagreek{U}}
\renewcommand{\isasymPhi}{\isagreek{F}}
\renewcommand{\isasymPsi}{\isagreek{Y}}
\renewcommand{\isasymOmega}{\isagreek{W}}

}
\isabellestyle{sf}

% todo compared to the original isabelle.sty, we have omitted some vertical
% spacing and forced \par's -- check if we really want this in the end...
%
% The problems we tried to fix with the current solution is that `unmotivated'
% vertical space appeared between alternations of "(*<*)...(*>*)" and "text {*
% ... *}", which is not acceptable and must otherwise be fixed manually by
% reordering the material in the theories.
\renewcommand{\isabeginpar}{}
\renewcommand{\isaendpar}{}
\makeatletter
\renewenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
\makeatother

\DeclareRobustCommand\ensuretext[1]{\ifmmode\text{#1}\else{#1}\fi}

\newcommand{\freefnt}[1]{\textsl{\rmfamily#1}}
\newcommand{\boundfnt}[1]{{\textsl{\sffamily#1}}}
\newcommand{\constructorfnt}[1]{\textsc{#1}}
\newcommand{\holkeywordfnt}[1]{\texttt{#1}}

\newcommand{\tfreeify}[1]{\ensuretext{\freefnt{#1}}}
\newcommand{\freeify}[1]{\ensuretext{\freefnt{#1}}}
\newcommand{\boundify}[1]{\ensuretext{\boundfnt{#1}}}
\newcommand{\constructor}[1]{\ensuretext{\constructorfnt{#1}}}
\newcommand{\holkeyword}[1]{\ensuretext{\holkeywordfnt{#1}}}


\newcommand{\isasymllceil}{\isamath{\llceil}}
\newcommand{\isasymrrceil}{\isamath{\rrceil}}
\renewcommand{\isasymturnstile}{\isamath{\,\vdash}}
\renewcommand{\isasymTurnstile}{\isamath{\,\models}}
\newcommand{\isastring}[1]{``#1''}
\newcommand{\accessor}[1]{\isa{the}$_{\textsc{#1}}$}
\newcommand{\isaclike}[1]{\texttt{#1}}

\renewcommand{\isasymvv}{\mbox{\isastyleminor\isastylescript v+1}}
% include pdfcolor when using pdflatex
%\ifpdf
%  \input pdfcolor.tex
%\fi

\newcommand{\listty}[1]{%
  \ensuremath{\mathit{\id{#1} \ \id{list}  } } }

\newcommand{\texth}{\mathcode`\-=`\-\relax}


\newcommand{\id}[1]{%
  \ensuremath{\mathit{\texth#1}}}


\newcommand{\co}[1]{%
  \ensuremath{\mathsf{\texth#1}}}


\newcommand{\rf}[1]{%
  \ensuremath{\mathsf{#1}}}

\newcommand{\Some}[1]{%
  \ensuremath{\mathit{\left\lfloor #1 \right\rfloor} } }

\newcommand{\cons}[1]{%
  \ensuremath{\mathsf{#1}}}

% TODO: improve typesetting of formulas. use Isabelle's document generation? if so remove the following macro definitions
% some macro's
\DeclareRobustCommand{\listlength}[1]{\left|#1\right|} % Isabelle: length
\DeclareRobustCommand{\MemConfLM}{\ensuremath{\id{lm}}\xspace}
\DeclareRobustCommand{\recursiondepth}[1]{\listlength{#1.\MemConfLM}}
\DeclareRobustCommand{\heapbase}{\ensuremath{\id{abase}_\text{heap}}\xspace} % Isabelle: heap_base, heap_base_word
\DeclareRobustCommand{\maxheapsize}{\ensuremath{\id{asize}_\text{heap}^\text{max}}\xspace} % Isabelle: heap_size_max
\DeclareRobustCommand{\maxheap}{\ensuremath{\heapbase+\maxheapsize}\xspace} % Isabelle: max_heap
\DeclareRobustCommand{\intwdasnat}{\ensuremath{\id{i2n}}\xspace} % Isabelle: intwd_as_nat
\DeclareRobustCommand{\gprs}{\ensuremath{\id{gpr}}\xspace}
\DeclareRobustCommand{\heaptopreg}{\ensuremath{r_\text{htop}}\xspace} % Isabelle: heaptop_reg
\DeclareRobustCommand{\lastframereg}{\ensuremath{r_\text{lframe}}\xspace} % Isabelle: last_frame_reg
\DeclareRobustCommand{\sbasereg}{\ensuremath{r_\text{sbase}}\xspace} % Isabelle: sbase_reg
\DeclareRobustCommand{\sbasebubble}{\ensuremath{\id{bubble}_\text{code}}\xspace} % Isabelle: sbase_bubble
\DeclareRobustCommand{\computesbase}{\ensuremath{\id{abase}_\text{gm}}\xspace} % Isabelle: compute_sbase
\DeclareRobustCommand{\programbase}{\ensuremath{\id{progbase}}\xspace} % Isabelle: program_basee, program_base_word
\DeclareRobustCommand{\stackframebubble}{\ensuremath{\id{bubble}_\text{gm}}\xspace} % Isabelle: stack_frame_bubble
\DeclareRobustCommand{\abaselocalframe}{\ensuremath{\id{abase}_\text{lm}}\xspace} % Isabelle: abase_local_frame
\DeclareRobustCommand{\tenv}{\ensuremath{\id{te}}\xspace}
\DeclareRobustCommand{\pt}{\ensuremath{\id{ft}}\xspace}
\DeclareRobustCommand{\extractsymbolconf}{\ensuremath{\id{sc}}\xspace} % Isabelle: extract_symbolconf
\DeclareRobustCommand{\stackstart}{\abaselocalframe} % Isabelle: stack_start
\DeclareRobustCommand{\gmsymbols}{\ensuremath{\id{gst}}\xspace} % Isabelle: gm_symbols


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%


\def\listith{\id{!}}

\def\implies {\ensuremath{\Rightarrow}}

\def\ibool {\id{bool}}
\def\inat{\Nat}

\def\iff {\textbf{if }}
\def\then {\textbf{then}}
\def\elseif {\textbf{else}}

\def\case{\id{\textbf{case}}}
\def\of{\id{\textbf{ of }}}

\def\indef{\id{\textbf{in }}}
\def\letdef{\id{\textbf{let }}}

\def\undef{\id{undef}}
\def\funnames{\id{fun_n}}



\def\cc {\id{c}}
\def\sczero {\id{c0}}
\def\confc {\ensuremath{\mathit{C_{\rm{co}}}}}
\def\deltac {\ensuremath{\mathit{\delta_\sczero}}}

\newcommand{\Def}[1]{\emph{#1}}




\sloppy
% The following is enclosed to allow easy detection of differences in
% ascii coding.
% Upper-case    A B C D E F G H I J K L M N O P Q R S T U V W X Y Z
% Lower-case    a b c d e f g h i j k l m n o p q r s t u v w x y z
% Digits        0 1 2 3 4 5 6 7 8 9
% Exclamation   !           Double quote "          Hash (number) #
% Dollar        $           Percent      %          Ampersand     &
% Acute accent  '           Left paren   (          Right paren   )
% Asterisk      *           Plus         +          Comma         ,
% Minus         -           Point        .          Solidus       /
% Colon         :           Semicolon    ;          Less than     <
% Equals        =3D           Greater than >          Question mark ?
% At            @           Left bracket [          Backslash     \
% Right bracket ]           Circumflex   ^          Underscore    _
% Grave accent  `           Left brace   {          Vertical bar  |
% Right brace   }           Tilde        ~


\newcommand{\Nat}{{\mathbb N}}
\newcommand{\Real}{{\mathbb R}}
\def\lastname{Schirmer}
\pagestyle{plain}

\setcounter{tocdepth}{3}
\begin{document}
%\begin{frontmatter}

  \title{A Reduction Theorem for Store Buffers}

  \author{Ernie Cohen\inst{1}, Norbert Schirmer\inst{2}\fnmsep\thanks{Work funded by the German Federal Ministry of Education and Research (BMBF) in the framework of the Verisoft XT project under grant 01 IS 07 008.}}

\institute{Microsoft Corp., Redmond, WA, USA
\and German Research Center for Artificial Intelligence (DFKI) Saarbr\"ucken, Germany\\
\email{ecohen@amazon.com}, \email{norbert.schirmer@web.de}}

\maketitle


\begin{abstract}

When verifying a concurrent program, it is usual to assume that memory
is sequentially consistent.  However, most modern multiprocessors
depend on store buffering for efficiency, and provide native
sequential consistency only at a substantial performance penalty.  To
regain sequential consistency, a programmer has to follow an
appropriate programming discipline. However, na\"ive disciplines,
such as protecting all shared accesses with locks, are not flexible
enough for building high-performance multiprocessor software.

We present a new discipline for concurrent programming under TSO
(total store order, with store buffer forwarding). It does not depend
on concurrency primitives, such as locks. Instead, threads use ghost
operations to acquire and release ownership of memory addresses. A
thread can write to an address only if no other thread owns it, and
can read from an address only if it owns it or it is shared and the thread
has flushed its store buffer since it last wrote to an address it did
not own. This discipline covers both coarse-grained concurrency (where
data is protected by locks) as well as fine-grained concurrency (where
atomic operations race to memory).

We formalize this discipline in Isabelle/HOL, and prove that if every
execution of a program in a system without store buffers follows the
discipline, then every execution of the program with store buffers is
sequentially consistent. Thus, we can show sequential consistency
under TSO by ordinary assertional reasoning about the program, without
having to consider store buffers at all.

\end{abstract}

\tableofcontents
%\begin{keyword}
%Pervasive formal verification, systems verification, software verification, theorem proving
%\end{keyword}
%\end{frontmatter}

\section{Introduction \label{sec:introduction}}

When verifying a shared-memory concurrent program, it is usual to
assume that each memory operation works directly on a shared memory
state, a model sometimes called \Def{atomic} memory. A memory
implementation that provides this abstraction for programs that
communicate only through shared memory is said to be \Def{sequentially
  consistent}. Concurrent algorithms in the computing literature
tacitly assume sequential consistency, as do most application
programmers.

However, modern computing platforms typically do not guarantee
sequential consistency for arbitrary programs, for two reasons. First,
optimizing compilers are typically incorrect unless the program is
appropriately annotated to indicate which program locations might be
concurrently accessed by other threads; this issue is addressed only
cursorily in this report. Second, modern processors buffer stores of
retired instructions. To make such buffering transparent to
single-processor programs, subsequent reads of the processor read from
these buffers in preference to the cache. (Otherwise, a program could
write a new value to an address but later read an older value.)
However, in a multiprocessor system, processors do not snoop the store
buffers of other processors, so a store is visible to the storing
processor before it is visible to other processors. This can result in
executions that are not sequentially consistent.

The simplest example illustrating such an inconsistency is the
following program, consisting of two threads T0 and T1, where
\texttt{x} and \texttt{y} are shared memory variables (initially 0)
and \texttt{r0} and \texttt{r1} are registers:
%
\begin{center}
\begin{minipage}{6cm}
\begin{multicols}{3}
T0
\begin{verbatim}
x = 1;
r0 = y;
\end{verbatim}

\columnbreak

T1
\begin{verbatim}
y = 1;
r1 = x;
\end{verbatim}
\columnbreak

\end{multicols}
\end{minipage}
\end{center}
%
In a sequentially consistent execution, it is impossible for both
\texttt{r0} and \texttt{r1} to be assigned $0$. This is because the
assignments to \texttt{x} and \texttt{y} must be executed in some
order; if \texttt{x} (resp. \texttt{y}) is assigned first, then
\texttt{r1} (resp. \texttt{r0}) will be set to $1$. However, in the
presence of store buffers, the assignments to \texttt{r0} and
\texttt{r1} might be performed while the writes to \texttt{x} and
\texttt{y} are still in their respective store buffers, resulting in
both \texttt{r0} and \texttt{r1} being assigned $0$.

One way to cope with store buffers is make them an explicit part of
the programming model. However, this is a substantial programming
concession. First, because store buffers are FIFO, it ratchets up the
complexity of program reasoning considerably; for example, the
reachability problem for a finite set of concurrent finite-state
programs over a finite set of finite-valued locations is in PSPACE
without store buffers, but undecidable (even for two threads) with
store buffers. Second, because writes from function calls might still
be buffered when a function returns, making the store buffers explicit
would break modular program reasoning.

In practice, the usual remedy for store buffering is adherence to a
programming discipline that provides sequential consistency for a
suitable class of architectures. In this report, we describe and prove
the correctness of such a discipline suitable for the memory model
provided by existing x86/x64 machines, where each write emerging from
a store buffer hits a global cache visible to all processors. Because
each processor sees the same global ordering of writes, this model is
sometimes called \Def{total store order}
(TSO)\cite{Adve:Computer-29-12-66}\footnote{Before 2008, Intel
\cite{IntelWhitePaper} and AMD \cite{AMD:AMD64A2006-ALL} both put
forward a weaker memory model in which writes to different memory
addresses may be seen in different orders on different processors, but
respecting causal ordering. However, current implementations satisfy
the stronger conditions described in this report and are also
compliant with the latest revisions of the Intel specifications
\cite{Intel:IIA2006-ALL}. According to Owens et
al. \cite{Owens:TPHOL09-?} AMD is also planning a similar adaptation
of their manuals.}

The concurrency discipline most familiar to concurrent programs is one
where each variable is protected by a lock, and a thread must hold the
corresponding lock to access the variable. (It is possible to
generalize this to allow shared locks, as well as variants such as
split semaphores.) Such lock-based techniques are typically referred
to as \Def{coarse-grained} concurrency control, and suffice for most
concurrent application programming. However, these techniques do not
suffice for low-level system programming (\eg the construction of OS
kernels), for several reasons. First, in kernel programming efficiency
is paramount, and atomic memory operations are more efficient for many
problems. Second, lock-free concurrency control can sometimes
guarantee stronger correctness (\eg wait-free algorithms can provide
bounds on execution time). Third, kernel programming requires taking
into account the implicit concurrency of concurrent hardware
activities (\eg a hardware TLB racing to use page tables while the
kernel is trying to access them), and hardware cannot be forced to
follow a locking discipline.

A more refined concurrency control discipline, one that is much closer
to expert practice, is to classify memory addresses as lock-protected
or shared. Lock-protected addresses are used in the usual way, but
shared addresses can be accessed using atomic operations provided by
hardware (e.g., on x86 class architectures, most reads and writes are
atomic\footnote{This atomicity isn't guaranteed for certain memory types,
  or for operations that cross a cache line.}). The main restriction
on these accesses is that if a processor does a shared write and a subsequent
shared read (possibly from a different address), the processor must
flush the store buffer somewhere in between. For example, in the
example above, both \texttt{x} and \texttt{y} would be shared
addresses, so each processor would have to flush its store buffer
between its first and second operations.

However, even this discipline is not very satisfactory. First, we would
need even more rules to allow locks to be created or destroyed, or to
change memory between shared and protected, and so on.  Second, there
are many interesting concurrency control primitives, and many
algorithms, that allow a thread to obtain exclusive ownership of a
memory address; why should we treat locking as special?

In this report, we consider a much more general and powerful
discipline that also guarantees sequential consistency. The basic rule
for shared addresses is similar to the discipline above, but there are
no locking primitives. Instead, we treat \Def{ownership} as
fundamental. The difference is that ownership is manipulated by
nonblocking ghost updates, rather than an operation like locking that
have runtime overhead. Informally the rules of the discipline are as
follows:
\begin{itemize}
\item In any state, each memory address is either \Def{shared} or
  \Def{unshared}. Each memory address is also either \Def{owned} by a
  unique thread or \Def{unowned}. Every unowned address must be
  shared. Each address is also either read-only or read-write.
  Every read-only address is unowned.
\item A thread can (autonomously) acquire ownership of an unowned
  address, or release ownership of a address that it owns. It can also
  change whether an address it owns is shared or not. Upon release of
  an address it can mark it as read-only.
\item Each memory access is marked as \Def{volatile} or
  \Def{non-volatile}.
\item A thread can perform a write if it is \Def{\Sound}. It can
  perform a read if it is sound and \Def{clean}.
\item A non-volatile write is \Sound\ if the thread owns the address
  and the address is unshared.
\item A non-volatile read is \Sound\ if the thread owns the address or the address is read-only.
\item A volatile write is \Sound\ if no other thread owns the address
  and the address is not marked as read-only.
\item A volatile read is \Sound\ if the address is shared or the thread owns it.
\item A volatile read is clean if the store buffer has been flushed since the
  last volatile write.  Moreover, every non-volatile read is clean.
\item For interlocked operations (like compare and swap), which have
  the side effect of the store buffer getting flushed, the rules for
  volatile accesses apply.
\end{itemize}

Note first that these conditions are not thread-local, because some actions
are allowed only when an address is unowned, marked read-only, or not
marked read-only. A thread can ascertain such conditions only through
system-wide invariants, respected by all threads, along with data it
reads. By imposing suitable global invariants, various thread-local
disciplines (such as one where addresses are protected by locks,
conditional critical reasons, or monitors) can be derived as lemmas by
ordinary program reasoning, without need for meta-theory.

Second, note that these rules can be checked in the context of a
concurrent program without store buffers, by introducing ghost state
to keep track of ownership and sharing and whether the thread has performed a volatile write
since the last flush. Our main result is that if a program obeys the rules
above, then the program is sequentially consistent when executed on a
TSO machine.

Consider our first example program. If we choose to leave both
\texttt{x} and \texttt{y} unowned (and hence shared), then all accesses must be volatile.
This would force each thread to flush the store buffer between their
first and second operations.  In practice, on an x86/x64 machine, this
would be done by making the writes interlocked, which flushes store
buffers as a side effect.  Whichever thread flushes its store buffer
second is guaranteed to see the write of the other thread, making the
execution violating sequential consistency impossible.

However, couldn't the first thread try to take ownership of \texttt{x}
before writing it, so that its write could be non-volatile? The answer
is that it could, but then the second thread would be unable to read
\texttt{x} volatile (or take ownership of \texttt{x} and read it
non-volatile), because we would be unable to prove that \texttt{x} is
unowned at that point.  In other words, a thread can take ownership of
an address only if it is not racing to do so.

Ultimately, the races allowed by the discipline involve volatile
access to a shared address, which brings us back to locks.  A spinlock
is typically implemented with an interlocked read-modify-write on an
address (the interlocking providing the required flushing of the store
buffer).  If the locking succeeds, we can prove (using for example a
ghost variable giving the ID of the thread taking the lock) that no
other thread holds the lock, and can therefore safely take ownership
of an address ``protected'' by the lock (using the global invariant
that only the lock owner can own the protected address).  Thus, our
discipline subsumes the better-known disciplines governing
coarse-grained concurrency control.

To summarize, our motivations for using ownership as our core notion of a
practical programming discipline are the following:
\begin{enumerate}
\item the distinction between global (volatile) and local (non-volatile) accesses is a practical requirement to
reduce the performance penalty due to necessary flushes and to allow important compiler optimizations
(such as moving a local write ahead of a global read),
\item coarse-grained concurrency control like locking is nothing special but only a derived concept which is
used for ownership transfer (any other concurrency control that guarantees exclusive access is also fine), and
\item we want that the conditions to check for the programming discipline can be discharged by ordinary state-based
program reasoning on a sequentially consistent memory model
(without having to talk about histories or complete executions).
\end{enumerate}

\paragraph{Overview}
In Section \ref{sec:preliminaries} we introduce preliminaries of
Isabelle/HOL, the theorem prover in which we mechanized our work. In
Section \ref{sec:discipline} we informally describe the programming
discipline and basic ideas of the formalization, which is detailed in
Section \ref{sec:formalization} where we introduce the formal models and the
reduction theorem.
In Section \ref{sec:buildingblocks} we give some details of important building blocks
for the proof of the reduction theorem.
To illustrate the connection between a programming language semantics and our reduction theorem, we instantiate our
framework with a simple semantics for a parallel WHILE language in Section \ref{sec:pimp}.
Finally we conclude in Section \ref{sec:conclusion}.

\input{Preliminaries.tex}
%\input{thy/document/Text.tex}
\input{Text.tex}

\section{Conclusion \label{sec:conclusion}}

We have presented a practical and flexible  programming
discipline for concurrent programs that ensures sequential consistency on TSO machines, such
as present x64 architectures. Our approach covers a wide
variety of concurrency control, covering locking, data races, single
writer multiple readers, read only and thread local portions of
memory.  We minimize the need for store buffer flushes to optimize the
usage of the hardware.  Our theorem is not coupled to a specific
logical framework like separation logic but is based on more
fundamental arguments, namely the adherence to the programming discipline
which can be discharged within any program logic using the standard sequential
consistent memory model,  without any of the complications of TSO.

\paragraph{Related work.}

\emph{Disclaimer.}
This contribution presents the state of our work from 2010 \cite{Cohen:ITP2010-}.
Finally, 8 years later, we made the AFP submission for Isabelle2018.
This related work paragraph does not thoroughly cover publications that came up in the meantime.


A categorization of various weak memory models is presented in
\cite{Adve:Computer-29-12-66}.  It is
compatible with the recent revisions of the Intel manuals
\cite{Intel:IIA2006-ALL} and the revised x86 model presented in
\cite{Owens:TPHOL09-?}.  The state of the art in formal verification
of concurrent programs is still based on a sequentially consistent
memory model.  To justify this on a weak memory model often a quite
drastic approach is chosen, allowing only coarse-grained concurrency
usually implemented by locking. Thereby data races are ruled out
completely and there are results that data race free programs can be
considered as sequentially consistent for example for the Java memory
model \cite{DBLP:conf/ecoop/SevcikA08,DBLP:conf/tphol/AspinallS07} or
the x86 memory model\cite{Owens:TPHOL09-?}.  Ridge
\cite{conf/tphol/Ridge07} considers weak memory and data-races and
verifies Peterson's mutual exclusion algorithm. He ensures
sequentially consistency by flushing after every write to shared
memory.
%
Burckhardt and Musuvathi\cite{Sober} describe an execution monitor that
efficiently checks whether a sequentially consistent TSO execution has a single-step
extension that is not sequentially consistent. Like our approach, it
avoids having to consider the store buffers as an explicit part of the
state. However, their condition requires maintaining in ghost state
enough history information to determine causality between events,
which means maintaining a vector clock (which is itself unbounded) for
each memory address. Moreover, causality (being essentially graph
reachability) is already not first-order, and hence unsuitable for
many types of program verification.
%
Closely related to our work is the draft of Owens~\cite{Owens-draft} which also
investigates on the conditions for sequential consistent reasoning within TSO.
The notion of a \emph{triangular-race} free trace is established to exactly
characterize the traces on a TSO machine that are still sequentially consistent.
A triangular race occurs between a read and a write of two different threads to the
same address, when the reader still has some outstanding writes in the store buffer.
To avoid the triangular race the reader has to flush the store buffer before reading.
This is essentially the same condition that our framework enforces, if we limit
 every address to be unowned and every access to be volatile.
We regard this limitation as too strong for practical programs, where non-volatile accesses
(without any flushes) to temporarily local portions of memory (e.g. lock protected data) is common practice.
This is our core motivation for introducing the ownership based programming discipline.
%
We are aware of two extensions of our work that were published in the meantime.
Chen \textit{et al}.~\cite{chen-2014} also take effects of the MMU into account and generalize our reduction theorem to handle programs that edit page tables.
Oberhauser~\cite{Oberhauser-2016} improves on the flushing policy to also take non-triangular races into account and facilitates an alternative proof approach.


\paragraph{Limitations.}
There is a class of important programs that are not sequentially consistent but nevertheless correct.

First consider a simple spinlock implementation with a volatile lock \texttt{l}, where \texttt{l == 0}
indicates that the lock is not taken. The following code acquires the lock:
\begin{verbatim}
  while(!interlocked_test_and_set(l));
  <critical section accessing protected objects>,
\end{verbatim}
and with the assignment \texttt{l = 0} we can release the lock again.
Within our framework address \texttt{l} can be considered \emph{unowned} (and hence shared) and every access to it
is \emph{volatile}.
We do not have to transfer ownership of the lock \texttt{l} itself but of the objects it protects.
As acquiring the lock is an expensive interlocked oprations anyway there are no additional restrictions from our framework.
The interesting point is the release of the lock via the volatile write \texttt{l=0}.
This leaves the dirty bit set, and hence our programming discipline requires a flushing instruction before the
next volatile read.
If \texttt{l} is the only volatile variable this is fine, since the next operation will be a lock acquire again which is interlocked and thus flushes the store buffer.
So there is no need for an additonal fence.
But in general this is not the case and we would have to insert a fence after the lock release to make the dirty bit clean again and to stay sequentially consistent. However, can we live without the fence? For the correctness of the mutal-exclusion algorithm we can, but we leave the domain of sequential consistent reasoning.
The intuitive reason for correctness is that the threads waiting for the lock do no harm while waiting. They only take some action if they see the lock being zero again, this is when the lock release has made its way out of the store buffer.

Another typical example is the following simplified form of
barrier synchronization: each processor has a flag that it writes (with ordinarry volatile writes without any flushing)
and other processors read, and each processor waits for all processors to
set their flags before continuing past the barrier. This is not
sequentially consistent -- each processor might see his own flag set
and later see all other flags clear -- but it is still correct.

Common for these examples is that there is only a single writer to an address,
and the values written are monotonic in a sense that allows the readers to draw the correct conlcusion
when they observe a certain value. This pattern is named
\emph{Publication Idiom} in Owens work~\cite{Owens-draft}.




\paragraph{Future work.}
The first direction of future work is to try to deal with the limitations
of sequential consistency described above and try to come up with a more general reduction
theorem that can also handle non sequential consistent code portions that follow some
monotonicity rules.

Another direction of future work is to take compiler optimization into
account. Our volatile accesses correspond roughly to volatile memory
accesses within a C program. An optimizing compiler is free to convert
any sequence of non-volatile accesses into a (sequentially
semantically equivalent) sequence of accesses. As long as execution is
sequentially consistent, equivalence of these programs (\eg with
respect to final states of executions that end with volatile
operations) follows immediately by reduction. However, some compilers
are a little more lenient in their optimizations, and allow operations
on certain local variables to move across volatile operations. In the
context of C (where pointers to stack variables can be passed by
pointer), the notion of ``locality'' is somewhat tricky, and makes
essential use of C forbidding (semantically) address arithmetic across
memory objects.

\section*{Acknowledgements}
We thank Mark Hillebrand for discussions and feedback on this work and
extensive comments on this report.

\appendix
\section{Appendix}
After the explanatory text in the main body of the document we now show the plain theory files.

\input{ReduceStoreBuffer.tex}
\input{ReduceStoreBufferSimulation.tex}
\input{PIMP.tex}

\bibliographystyle{plain}
\bibliography{root}

%\pagebreak
%\appendix
%\input{thy/document/Appendix.tex}
\end{document}
