-
Notifications
You must be signed in to change notification settings - Fork 0
/
intro.tex
74 lines (65 loc) · 4.77 KB
/
intro.tex
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
\section{Introduction}
Software and hardware systems are required to be reliable.
For example, space satellites must be able to operate autonomously in space,
adapting to short term and long term changes,
with required lifetimes in the order of decades, whereas
one"/minute downtime failure of banking software may lead to significant expenses.
Software reliability may be achieved through testing and post"/design quality
assurance, but there is always a possibility to leave some branches of an operation
scenario untested, leading to a potential disaster~\cite{Leveson2004}.
In contrast with post"/design testing, which does not provide the full
correctness guarantee, formal methods yield a systematic approach for developing
complex systems in a correct"/by"/construction manner. One reason for advancement
of formal methods in comparison to testing is a maximal possible elimination of
human errors. For instance, automated theorem provers perform exhaustive search
through the entire space of possible states of the system and~\emph{formally prove} its
operation to be correct in every single case, completely excluding any possibility of
non"/specified execution (presuming the correctness of a specification).
Formal verification is performed by means of a verification tool,
a~\emph{verification metalanguage} that is used to formalise the model of the system.
However, the development of formal verification tools is by itself a hard problem.
There is little to no escape from the \emph{barber paradox} here\footnote{
The barber is the "one who shaves all those, and those only, who do not shave themselves."~
The question is, does the barber shave himself? In the formal verification context, the
verification framework is the barber.}, therefore most formal
verification tools have a~\emph{trusted core} --- a part of the implementation that
is not itself verified. This fact obliges the developers of a verification framework
to constantly evaluate the correctness of the implementation. Thus, it is vital
to keep the trusted core implementation clear and as concise as possible. This report
is dedicated to a case study of development of a simulation and formal verification
framework in the domain of computer architecture.
The IAM\footnote{The acronym IAM stands for Inglorious Adding Machine.} instruction
set architecture is designed to be a case study for the development of simulation
and formal verification tools. Thus, the design of the Instruction Set
Architecture~(ISA) of IAM is mainly driven by the dichotomy between the tool
expressiveness and the implementation conciseness.
We want the tool implementation to be reasonably concise in order to keep the
focus on the implementation details and escape the mental overhead of maintaining
a large code base. At the same time, the case study must be sophisticated enough
to yield interesting programs with non-trivial properties to be verified.
The IAM design was inspired by an extreme case of one instruction
set computers (OISCs). OISCs have ISAs consisting from one instruction only and are
beautiful in their simplicity. But the verification tool implemented for such a
simple case would be too degenerated; thus we enriched the architecture with a
limited set of additional instructions.
In this report we present the IAM architecture and a Haskell framework for
simulation, formal verification and synthesis of IAM programs.
The framework includes an embedded assembly language and support for
simulating the machine operation and verifying properties of the IAM programs. As
IAM architecture design is mainly driven by our Haskell implementation, we
present all the involved concepts using their Haskell encoding. We believe that
Haskell notation is clear enough and the chosen manner of presentation will
enable us to focus on the formal verification framework implementation.
IAM has 4 general purpose registers, 2 flags and 8 instructions. It
operates on 64-bit words as data values and uses 8-bit words as memory addresses.
Some instructions expect an 8-bit signed immediate argument.
This report is structured as following: we first consider the representation of
the instruction syntax (section ~\ref{sec:Instructions}) and informally describe the intuitive meaning of each
instruction; then we transfer to the model of machine state and execution (section~\ref{sec:State}),
gradually building an interpreter for instructions in terms of transitions
between IAM's states. We continue with the description of an embedded assembly
language (section~\ref{sec:Assembly}) that enables us to build IAM programs reusing Haskell's syntax.
Section~\ref{sec:Semantics} formally defines the meaning of IAM instructions in terms of state transformers.
The last section (\ref{sec:Verification}) presents examples of usage of the developed simulation
and formal verification framework.
\clearpage