Transcript Abstract State Machines: From Foundations to Tools

Abstract State Machines,
and lessons of
an ASM-based project at Microsoft
Yuri Gurevich (Erdos #2)
Microsoft Research
Modeling
No science without modeling


The virtuous cycle
Maybe even no life without modeling
Physics uses PDEs for modeling.
What are the PDEs of computer science?
2
Turing’s analysis of computation
Great
Yet limited
3
Improving on Turing’s analysis
Emile Post
Andrei Kolmogorov
“Algorithms compute in steps
of bounded complexity.”
Pointer machines
Robin Gandy
4
Another line of analysis
Recursive functions
Skolem to Gödel
Lambda calculus
Church’s thesis
Comparing the two
lines
5
A Thought Experiment
A perfect machine model
Step-for-step simulation
of any algorithm
Uses: software specs,
model based testing
What would the model look
like?
6
Postulate 1: Sequential Time
An algorithm is a
transition system.
What are states?
What are
transitions?
7
States
The state is information that, given
the program, determines the ensuing
computation(s).

More than the values of the variables.
What is the form of states?

Or what is is?
8
Postulate 2: Abstract State
The states are structures
in the sense of mathematical logic.



Same vocabulary
Transitions preserve the state domain.
Everything is preserved under isomorphism.
9
What are
transitions?
Deterministic or nondeterministic?
More generally,
interactive or non-interactive?
Let’s consider first the classical case of
non-interactive algorithms.
10
What are transitions? (cont.)
How powerful steps are?
Let’s consider first the classical case of
“steps of bounded complexity.”
How to bound the complexity?
11
Locations and updates
Locations  = (f,(a1,..,aj))
Content() = f(a1,..,aj)
Updates (,v)
The update set of state X is
(X) =
{ (,v) : v = Content() in Next(X)
 Content() in X
}
12
Postulate 3: Bounded Exploration
There is a finite set t1,..,tn
of critical terms such that
(X) = (Y) if every ValX(ti) = ValY(ti).
13
Definition
A sequential algorithm is
an abstract-state bounded-exploration
transition system.
14
Sequential ASMs
Syntax
f(t1,..,tj):= t0
Semantics
=?
{(,a0)} where
=(f,(a1,..,aj)) and
each ai = Val(ti)
do in parallel
R1 … Rk
(R1)  …  (Rk)
if t then R1
else R2
if Val(t) = true then (R1)
else (R2)
15
Example
if b = 0 then d := a
else
[do in-parallel]
a := b
b := a mod b
Nullary dynamic functions:
Static functions:
a, b, d
=, 0, mod
16
Example (cont.)
if a(s)=0
d(s) :=
s
:=
else
a(s) :=
b(s) :=
then
b(s)
s+1
b(s) mod a(s)
a(s)
17
Seq Characterization Theorem
For any seq algorithm A
there is a seq ASM B such that
states of A are states of B and
every NextA(X) = NextB(X).
#141
18
Interaction
The ASM model is relatively
straightforward:

External functions

Choice and import operators
The from-the-first-principles analysis
is not straightforward.
19
In-place one-swap-a-time sorting
var A as Seq of Integer = [3,1,2]
Nondeterminsm
Swap()
choose i,j in Indices(A)
where i<j and A(i)>A(j)
A(i) := A(j)
A(j) := A(i)
A = [2,3,1]
A = [1,3,2]
A = [2,1,3]
Parallelism
Sort()
step until fixpoint
Swap()
A = [1,2,3]
20
Wide steps
Again, the ASM model is relatively
straightforward

do-for-all
The from-the-first-principles analysis
is not straightforward.
21
Topological Sorting Example
22
Distributed algorithms
Distributed ASMs were defined long
ago, but the axiomatization problem is
wide (and maybe forever) open.
To simulate, one can interleave (sets
of) actions of the computing agents.
23
Early ASM engines
ASM Workbench

Uni Paderborn, Siemens
ASM Gopher

Uni Ulm, Siemens
XASM

Uni Berlin, Kestrel
24
AsmL creators
In the hiring order: Wolfram Schulte, Margus
Veanes, Colin Campbell, Lev Nachmanson, Mike
Barnett, Wolfgang Grieskamp, Nikolai Tillmann
25
FSE propaganda example
Product Idea
/ Informal Spec
What product
are you
building?
Modeling
AsmL Model
Refinement
Are you
building the
right product?
Validation
Verification
Implementation
C, C++, C#, ...
Are you building
the product right ?
26
Spec
Validate
Enforce
Comprehend
Generate
test suites
Play scenarios
Test
Model check
On-the-fly testing
Lockstep runtime
verification
Prove properties
27
Conformance testing
Any
client
Discrepancies
flagged
I
Test harness
I
AsmL
model
I
Implementation
under test
28
Spec Explorer
Original purpose
Model based testing



Why model-based testing?
Arguably the largest model-based-testing
operation anywhere.
Success of sorts
29
Probability of
success
Coburn:
(pain of crisis)
divided by
(pain of adoption)
where pain means
perceived pain.
30
Love triangle
31