analyzing relational logicDaniel Jackson, MITWG 2.3 · NewcastleApril 2000
language assumptions
language
- first-order logic
- set & relation operators
- uninterpreted types
analysis desired
simulation
find a state that satisfies invariant J
and additionally condition C
- find an execution of operation O
resulting in a state satisfying P
from a state satisfying P
that changes the component x
that is not an execution of operation Ov
checking
- does invariant J imply invariant Jv?
- does operation O preserve invariant J ?
- does operation Oc refine Oa under abstraction A?
analyses not possible
refinement
- does Oc refines Oa for some abstraction?
- are all executions of O also executions of O1;O2?
spec by minimization
- make smallest change to connections that satisfies C
precondition checks
- does O have an execution from every state satisfying C?
temporal checks
- do reachable states satisfy J ?
semantics: formulas
M : formula ? env ? boolean
X : expr ? env ? value
env = (var + type) ? value
value = ? (atom ? atom) + (atom ? value)
M [a in b] e = X[a]e ? X[b]e
M [! F] e = ? M[F]e
M [F && G] e = M[F]e ? M[G]e
M [all v: t | F] e = ? {M[F] (e ? v ? x) | x ? e(t)}
semantics: expressions
X : expr ? env ? value
env = (var + type) ? value
value = ? (atom ? atom) + (atom ? value)
X [a + b] e = X[a]e ? X[b]e
X [a . b] e = {y | ?x. x ? X[a]e ? (x,y) ? X[b]e}
X [~a] e = {(x,y) | (y,x) ? X[a]e}
X [+a] e = the smallest r such that r ; r ? x ? X[a]e ? x
X [{v: t | F}] e = {x ? e(t) | M[F] (e ? v ? x)}
X [v] e = e(v)
X [a[v]] e = e(a)(v)
models
models are well-formed environments for which formula holds
M : formula ? env ? boolean
Models (F) = {e | M[f]e}
environment e is well formed iff
- tight: only bind variables declared along with formula
- type correct: if expression a has type T, X[a]e ? X[T]e
e is within scope k iff
- for all basic types T, #X[T]e = k
- write Modelsk (F) for models within scope k
small scope hypothesis
most bugs can be caught by considering only small instances
example
problem
a, b : S
p : S -> T
! (a b).p in (a.p b.p)
a model in a scope of 2
S = {S0, S1}
T = {T0, T1}
p = {(S0, T0), (S1, T0)}
a = {S0}
b = {S1}
what Alcoa does
alcoa : formula, scope ? env
- does not always succeed (ie, may return nothing)
properties
- termination: always, with deterministic solvers
- soundness: alcoa (F, k) ? Modelsk (F)
- relative completeness: Modelsk (F) ? {} ? alcoa (F, k) succeeds
non-properties
- minimality: alcoa (F, k) not the smallest model of F in k
- completeness: Models (F) ? {} ? alcoa (F, k) succeeds
so counterexamples are real, but cant prove theorems
scope monotonicity
Alcoa is scope monotonic
- alcoa (F, k) succeeds ? alcoa (F, k+1) succeeds
- if scope of 7 fails, no need to try 6, 5,
because models are scope monotonic
- Modelsk (F) ? Modelsk+1 (F)
- property of Alloy, not kernel
every analysis is model finding
does operation O preserve invariant J ?
alcoa (O && J && !J , 3)
show me how O1 and O2 differ
alcoa ((O1 && !O2) || (O2 && !O1) , 3)
show me an execution of O that changes x
alcoa architecture
overview of method
from alloy formula F and scope k generate
boolean formula BF
mapping ? : BoolAssignment ? Environment
such that
? maps every solution of BF
?n ? Modelsk (F) ? n ? Models (BF)
SAT solvers
in practice
- solvers work well for variables and ,000 clauses
- usually give small models
kinds of solver
- local search (eg, WalkSAT)
- Davis-Putnam (eg, RelSAT, SATO)
- non-clausal (eg, Prover)
example
problem
a, b : S
p : S -> T
! (a b).p in (a.p b.p)
translation in scope of 2
- formula becomes
- ((a0??b0 ? p00) ? (a1??b1 ? p10) ? ((a0 ? p00) ? (a1 ? p10)) ?? ((b0 ? p00) ? (b1 ? p10))) ?
- a model is
a0 , ?a1 , ?b0 , b1 , p00 , ?p01 , p10 , ?p11
mapping function ?
- set to vector of bool var
- relation to matrix
p [p00 p01 , p10 p11]
final result
S = {S0, S1}
T = {T0, T1}
p = {(S0, T0), (S1, T0)}
a = {S0}
b = {S1}
compositional translation
translating relation r: S -> T
XT [r]ij boolean var, true when r contains (Si, Tj)
translating expression e: T
XT [a]i boolean formula, true when a contains Ti
translating formulas
MT [F] boolean formula, true for models of F
sample rules
MT [F && G] = MT[F] ? MT[F]
XT [a - b]i = XT [a]i ? ?XT [b]i
XT [a . b]i = ?j. XT [a]j ? XT [b]ji
example
a [a0 a1]
b [b0 b1]
p [p00 p01 , p10 p11]
a b [a0??b0 a1??b1]
(a b).p [(a0??b0 ? p00) ? (a1??b1 ? p10)
]
a.p [(a0 ? p00) ? (a1 ? p10) (a0 ? p01) ? (a1 ? p11)]
b.p [(b0 ? p00) ? (b1 ? p10) (b0 ? p01) ? (b1 ? p11)]
a.p b.p [((a0 ? p00) ? (a1 ? p10)) ?? ((b0 ? p00) ? (b1 ? p10))
]
! (a b).p in (a.p b.p) ? (((a0??b0 ? p00) ? (a1??b1 ? p10) ? ((a0 ? p00) ? (a1 ? p10)) ?? ((b0 ? p00) ? (b1 ? p10)))) ?
quantifiers
example
!((all x | x in x.p) -> (all x | x in x.p.p))
put in negation normal form
(all x | x in x.p) && (some x | ! x in x.p.p)
skolemize
(all x | x in x.p) && ! (xc in xc.p.p)
how to translate remaining universal quantifiers?
environments & trees
semantics
M : formula ? env ? boolean
X : expr ? env ? value
env = (var + type) ? value
value = ? (atom ? atom) + (atom ? value)
translation
MT : formula ? boolFormula tree
XT : expr ? boolValue tree
? tree = (var ? (index ? ? tree) + ?
boolValue = booleanFormulaMatrix + (index ? boolValue)
env becomes (tree, boolean encoding of relations)
examples
compositional rules
MT [a in b] = merge (MT[a], MT[b], ?u,v. ?i (ui ? vj) )MT [all x | F] = fold (MT[F], ?)
merging
- subexpressions may have different variables
- so interpose layers as necessary, then merge
- maintain consistent ordering from root to leaf
symmetry
observation
- types are uninterpreted
- permuting elements of a type preserves modelhood
example
a = {S0} , b = {S1}, p = {(S0, T0), (S1, T0)}
a = {S1} , b = {S0}, p = {(S0, T0), (S1, T0)}
both models of !(a b).p in (a.p b.p)
exploitation
- environments form equivalence classes
- avoid considering all elements of a class
symmetry in boolean formula
preserved!
- express symmetry ? as permutation on boolean vars
- then ? is a symmetry of the boolean formula too
- want to rule out one of A, ?A
Crawfords idea
- order boolean vars into sequence V
- view assignments as binary numbers & pick smaller
- for each ?, add constraint V ? ?V
example
- A = 0123, ?A = 0123, ? = (02)
- V ? ?V is 0123 < 2103 = 0 < 2
symmetry constraint for a relation
suppose we translated relation p: S -> T to the matrix
symmetry (S0 S1) exchanges top two rows
constraint obtained is
0 1 2 3 4 5 6 7 8 < 3 4 5 0 1 2 6 7 8
= 0 1 2 < 3 4 5
= ?0?3 ? (0?3 ? ?1?4) ? (0?3 ? 1?4 ? ?2?5)
generalizing symmetry
extend to
- multiple relations and sets
- multiple types
but
- diminishing returns
- pick ordering of vars carefully
- homogeneous relations tricky
results
observations
- solver time dominates
- RelSAT dominates other solvers
- symmetry gives 100x speedup for proofs
- bugs in boolean code not translation
where are we?
- interactive analysis up to 200 bits
- small but real specs (longest so far is 400 lines)
- 30loc list-processing procedures
challenges
symmetry
- why do a few symmetries seem to work so well?
- what symmetries should be used?
progress bar
- will symmetry spoil our heuristics?
language extensions
- numbers (easy?)
- sequences (hard?)
PPT Slide
PPT Slide
PPT Slide