diff options
Diffstat (limited to 'doc')
| -rw-r--r-- | doc/Makefile | 10 | ||||
| -rw-r--r-- | doc/examples/my_replicate_bits.sail | 4 | ||||
| -rw-r--r-- | doc/introduction.tex | 69 | ||||
| -rw-r--r-- | doc/manual.tex | 11 | ||||
| -rw-r--r-- | doc/riscv.tex | 2 | ||||
| -rw-r--r-- | doc/usage.tex | 2 |
6 files changed, 58 insertions, 40 deletions
diff --git a/doc/Makefile b/doc/Makefile index b5a74dd6..ae542571 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -65,11 +65,15 @@ code_myreplicatebits.tex: examples/my_replicate_bits.sail grammar.tex: ../language/sail.ott ott -pp_grammar -tex_wrap false -tex_suppress_category I -tex_suppress_category D -tex_suppress_ntr terminals -tex_suppress_ntr formula -tex_suppress_ntr judgement -tex_suppress_ntr user_syntax -tex_suppress_ntr dec_comm -sort false -generate_aux_rules false -picky_multiple_parses true -i ../language/sail.ott -o grammar.tex +LATEXARG=manual.tex manual.pdf: grammar.tex introduction.tex usage.tex types.tex code_riscv.tex riscv.tex manual.tex manual.bib tutorial.tex code_myreplicatebits.tex - pdflatex manual.tex + pdflatex ${LATEXARG} bibtex manual - pdflatex manual.tex - pdflatex manual.tex + pdflatex ${LATEXARG} + pdflatex ${LATEXARG} + +anon_man: LATEXARG='\def\ANON{}\input{manual.tex}' +anon_man: manual.pdf clean: -rm manual.pdf diff --git a/doc/examples/my_replicate_bits.sail b/doc/examples/my_replicate_bits.sail index c9972cd6..8c3c9458 100644 --- a/doc/examples/my_replicate_bits.sail +++ b/doc/examples/my_replicate_bits.sail @@ -17,10 +17,14 @@ val operator >> = { val "or_vec" : forall 'n. (bits('n), bits('n)) -> bits('n) +val zero_extend = "zero_extend" : forall 'n 'm, 'm >= 'n. (bits('n), atom('m)) -> bits('m) + overload operator | = {or_vec} val my_replicate_bits : forall 'n 'm, 'm >= 1 & 'n >= 1. (int('n), bits('m)) -> bits('n * 'm) +val zeros = "zeros" : forall 'n. atom('n) -> bits('n) + function my_replicate_bits(n, xs) = { ys = zeros(n * length(xs)); foreach (i from 1 to n) { diff --git a/doc/introduction.tex b/doc/introduction.tex index 5969f34f..1f9d9dba 100644 --- a/doc/introduction.tex +++ b/doc/introduction.tex @@ -21,27 +21,27 @@ pseudocode, which has recently become machine-processed~\cite{Reid16}. For MIPS~\cite{MIPS64-II,MIPS64-III} there is also reasonably detailed pseudocode. -The behaviour of concurrent code is often described less well. In a -line of research from 2007--2018 we have developed mathematically -rigorous models for the allowed architectural envelope of concurrent -code, for x86, IBM Power, \riscv, and ARM, that have been reasonably -well validated by experimental testing and by discussion with the -vendors and -others~\cite{x86popl,tphols09,cacm,CAV2010,Alglave:2011:LRT:1987389.1987395,pldi105,pldi2012,micro2015,FGP16,mixed17}. -In the course of this, we have identified a number of subtle issues -relating to the interface between the intra-instruction semantics and -the inter-instruction concurrency -semantics~\cite{pldi105,pldi2012,micro2015,FGP16,mixed17}. For -example, the concurrency models, rather than treating each instruction -execution as an atomic unit, require exposed register and memory -events, knowledge of the potential register and memory footprints of -instructions, and knowledge of changes to those during execution. Our -early work in this area had hand-coded instruction semantics for quite -small fragments of the instruction sets, just enough for concurrency -litmus tests and expressed in various ad hoc ways. As our models have -matured, we have switched to modelling the intra-instruction semantics -more completely and in a style closer to the vendor-documentation -pseudocode, and Sail was developed for this. +%% The behaviour of concurrent code is often described less well. In a +%% line of research from 2007--2018 we have developed mathematically +%% rigorous models for the allowed architectural envelope of concurrent +%% code, for x86, IBM Power, \riscv, and ARM, that have been reasonably +%% well validated by experimental testing and by discussion with the +%% vendors and +%% others\anonymiseomit{~\cite{x86popl,tphols09,cacm,CAV2010,Alglave:2011:LRT:1987389.1987395,pldi105,pldi2012,micro2015,FGP16,mixed17}}. +%% In the course of this, we have identified a number of subtle issues +%% relating to the interface between the intra-instruction semantics and +%% the inter-instruction concurrency +%% semantics\anonymiseomit{~\cite{pldi105,pldi2012,micro2015,FGP16,mixed17}}. For +%% example, the concurrency models, rather than treating each instruction +%% execution as an atomic unit, require exposed register and memory +%% events, knowledge of the potential register and memory footprints of +%% instructions, and knowledge of changes to those during execution. Our +%% early work in this area had hand-coded instruction semantics for quite +%% small fragments of the instruction sets, just enough for concurrency +%% litmus tests and expressed in various ad hoc ways. As our models have +%% matured, we have switched to modelling the intra-instruction semantics +%% more completely and in a style closer to the vendor-documentation +%% pseudocode, and Sail was developed for this. Sail is intended: @@ -77,7 +77,7 @@ and generate: \item An internal representation of the fully type-annotated definition (a deep embedding of the definition) in a form that can be executed by the Sail interpreter. These are both expressed in - Lem~\cite{Lem-icfp2014,Lemcode}, a language of type, function, and + Lem\anonymiseomit{~\cite{Lem-icfp2014,Lemcode}}, a language of type, function, and relation definitions that can be compiled into OCaml and various theorem provers. The Sail interpreter can also be used to analyse instruction definitions (or partially executed instructions) to @@ -101,25 +101,26 @@ binary descriptions, although this is something we plan to add. Sail has been used to develop models of parts of several architectures: \begin{center} \begin{tabular}{|l|l|} \hline -ARMv8 (hand) & hand-written \\ \hline +% ARMv8 (hand) & hand-written \\ \hline ARMv8 (ASL) & generated from ARM's v8.3 public ASL spec \\ \hline -IBM Power & extracted/patched from IBM Framemaker XML \\ \hline +% IBM Power & extracted/patched from IBM Framemaker XML \\ \hline MIPS & hand-written \\ \hline CHERI & hand-written \\ \hline \riscv & hand-written \\ \hline \end{tabular} \end{center} -The ARMv8 (hand) and IBM Power models cover all user-mode instructions -except vector, float, and load-multiple instructions, without -exceptions; for ARMv8 this is for the A64 fragment. +%% The ARMv8 (hand) and IBM Power models cover all user-mode instructions +%% except vector, float, and load-multiple instructions, without +%% exceptions; for ARMv8 this is for the A64 fragment. -The ARMv8 (hand) model is hand-written based on the ARMv8-A -specification document~\cite{armarmv8,FGP16}, principally by Flur. +%% The ARMv8 (hand) model is hand-written based on the ARMv8-A +%% specification document\anonymiseomit{~\cite{armarmv8,FGP16}}, +%% principally by \anonymise{Flur}. -The Power model is based on an automatic extraction of pseudocode and -decoding data from an XML export of the Framemaker document source of -the IBM Power manual~\cite{Power2.06,micro2015}, with manual patching -as necessary, principally by Kerneis and Gray. +%% The Power model is based on an automatic extraction of pseudocode and +%% decoding data from an XML export of the Framemaker document source of +%% the IBM Power manual\anonymiseomit{~\cite{Power2.06,micro2015}}, with manual patching +%% as necessary, principally by \anonymise{Kerneis and Gray}. The ARMv8 (ASL) model is based on an automatic translation of ARM's machine-readable public v8.3 ASL specification\footnote{ARM v8-A @@ -135,7 +136,7 @@ which in turn drew on MIPS4000 and MIPS32~\cite{MIPS4000,MIPS32-I}. % The CHERI model is based on that and the CHERI ISA reference manual version~5~\cite{UCAM-CL-TR-891}. These two are both principally by -Norton-Wright; they cover all basic user and kernel mode MIPS features +\anonymise{Norton-Wright}; they cover all basic user and kernel mode MIPS features sufficient to boot FreeBSD, including a TLB, exceptions and a basic UART for console interaction. ISA extensions such as floating point are not covered. The CHERI model supports either 256-bit capabilities diff --git a/doc/manual.tex b/doc/manual.tex index 3b75b26a..d731ecd3 100644 --- a/doc/manual.tex +++ b/doc/manual.tex @@ -64,9 +64,17 @@ \title{The Sail instruction-set semantics specification language} +\ifdefined\ANON +\author{Anonymous} +\newcommand\anonymise[1]{\emph{redacted}} +\newcommand\anonymiseomit[1]{} +\else \author{Alasdair Armstrong \and Thomas Bauereiss \and Brian Campbell \and Shaked Flur \and Kathryn E. Gray \and Robert Norton-Wright \and Christopher Pulte \and Peter Sewell} +\newcommand\anonymise[1]{#1} +\newcommand\anonymiseomit[1]{#1} +\fi \maketitle @@ -80,7 +88,8 @@ \include{tutorial} -\include{types} +% Remove for now since incomplete +%\include{types} \bibliographystyle{unsrt} \bibliography{manual} diff --git a/doc/riscv.tex b/doc/riscv.tex index 2ecc69df..299a7bdd 100644 --- a/doc/riscv.tex +++ b/doc/riscv.tex @@ -137,4 +137,4 @@ end execute The actual code for this example, as well as our more complete \riscv\ specification can be found on our github at -\url{https://github.com/rems-project/sail/blob/sail2/riscv/riscv_duopod.sail}. +\anonymise{\url{https://github.com/rems-project/sail/blob/sail2/riscv/riscv_duopod.sail}}. diff --git a/doc/usage.tex b/doc/usage.tex index b7a47934..09d4b903 100644 --- a/doc/usage.tex +++ b/doc/usage.tex @@ -91,7 +91,7 @@ We have a separate document detailing how to generate Isabelle theories from Sail models, and how to work with those models in Isabelle, see: \begin{center} -\url{https://github.com/rems-project/sail/raw/sail2/snapshots/isabelle/Manual.pdf} +\anonymise{\url{https://github.com/rems-project/sail/raw/sail2/snapshots/isabelle/Manual.pdf}} \end{center} Currently there are generated Isabelle snapshots for some of our models in \verb+snapshots/isabelle+ in the Sail repository. These |