...
Alloy/Kodkod
...
and
...
Applications
...
Kodkod is an efficient SAT-based
...
constraint
...
solver
...
for
...
first
...
order
...
logic
...
with
...
relations,
...
transitive
...
closure,
...
and
...
partial
...
models.
...
It provides analyses for both satisfiable and unsatisfiable problems: finite model finder for the former and a minimal unsatisfiable core extractor for the latter. Kodkod has been used in many applications, including code checking, test-case generation, declarative configuration, and lightweight analysis of formal specifications written in Alloy, UML, and Isabelle/HOL.
This talk will focus on MemSAT, a recent application of Kodkod to debugging and reasoning about memory models. MemSAT takes as input an axiomatic specification of a memory model and a multi-threaded test program containing assertions. The test program and the assertions comprise a litmus test for the memory model
| Wiki Markup |
|---|
{html}—{html} |
an
...
illustrative
...
encoding
...
of
...
a
...
behavior
...
that
...
the
...
model
...
should
...
allow
...
or
...
prohibit.
...
Given
...
these
...
inputs,
...
the
...
tool
...
outputs
...
a
...
trace
...
of
...
the
...
program
...
for
...
which
...
the
...
assertions
...
are
...
satisfied
...
or,
...
if
...
no
...
such
...
trace
...
exists,
...
it
...
outputs
...
a
...
minimal
...
subset
...
of
...
the
...
program
...
and
...
memory
...
model
...
constraints
...
that
...
are
...
unsatisfiable.
...
MemSAT
...
has
...
been
...
applied
...
to
...
several
...
existing
...
memory
...
models
...
and
...
their
...
published
...
litmus
...
tests,
...
including
...
the
...
current
...
Java
...
Memory
...
Model
...
by
...
Manson
...
et
...
al.,
...
and
...
a
...
revised
...
version
...
of
...
it
...
by
...
Sevcik
...
and
...
Aspinall.
...
The
...
results
...
revealed
...
subtle
...
discrepancies
...
between
...
what
...
was
...
expected
...
and
...
the
...
actual
...
results
...
of
...
test
...
programs.
...
Emina Torlak, LogicBlox, Inc.,
...
Atlanta,
...
GA,
...
USA
...
Emina
...
Torlak
...
received
...
her
...
Ph.D.
...
(2009),
...
M.Eng.
...
(2004)
...
and
...
B.Sc.
...
(2003)
...
in
...
Computer
...
Science
...
from
...
MIT.
...
Her
...
primary
...
research
...
interests
...
are
...
in
...
the
...
development
...
and
...
application
...
of
...
scalable
...
tools
...
for
...
lightweight
...
formal
...
methods,
...
program
...
analysis,
...
debugging
...
and
...
testing.
...
She
...
designed
...
and
...
implemented
...
Kodkod,
...
a
...
relational
...
constraint
...
solver
...
with
...
numerous
...
applications
...
to
...
design
...
analysis,
...
code
...
checking,
...
test-case
...
generation,
...
and
...
declarative
...
configuration.
...
Emina
...
is
...
currently
...
a
...
Senior
...
Computer
...
Scientist
...
at
...
LogicBlox,
...
where
...
she
...
is
...
working
...
on
...
specification-based
...
testing
...
of
...
online
...
analytical
...
processing
...
applications.
...
Prior
...
to
...
joining
...
LogicBlox,
...
she
...
was
...
a
...
Research
...
Staff
...
Member
...
at
...
the
...
IBM
...
T.
...
J.
...
Watson
...
Research
...
Center,
...
where
...
her
...
work
...
focused
...
on
...
the
...
analysis
...
of
...
weak
...
memory
...
models,
...
symbolic
...
debugging,
...
and
...
resource
...
leak
...
detection.
...
| Attachments |
|---|
...
|
...
|
...