Transcript CSE244 Compiler (a.k.a. Programming Language Translation)

A Formal Treatment of an
Abstract Channel Implementation
Using Java Sockets and TCP
Chryssis Georgiou, University of Cyprus
Peter Musial, VeroModo, Inc.
Alexander Shvartsman, University of Connecticut
Elaine Sonderegger, University of Connecticut
Motivation
• Abstract models and specifications of distributed
systems allow formal reasoning about their safety
properties
• Mapping the functionality of abstract specifications
to executable code for target distributed platforms is
a challenging and error-prone process
• Formal specifications and faithful implementations
of asynchronous communication channels are
particularly challenging
2
Related Work
• Traditional communication channel models
– Fixed, pre-initialized channels
– Examples
• Reliable FIFO channel
• Lossy reordering channel
• Josh Tauber’s IOA compiler used Java/MPI to
implement pre-initialized channels
3
Our Work
• First formal specification of an asynchronous
communication channel with:
– Explicit initialization
– Dynamic interconnections with graceful comings and
goings
• Implementation of the specification using Java’s
interface to TCP sockets
• Proof by forward simulation that the implementation
preserves the safety properties of the specification
4
Initialization
Sender
Receiver
senderOpen
send
send
send
receiverListening
respReceiverListening
receive
receive
5
Sender Closing
emptying
closed
Sender
Receiver
senderClose
senderClosing
receive
receive
receive
6
Receiver Closing
closed
Sender
Receiver
receiverClose
Bit Bucket
7
Abstract Channel
• Input/Output Automata formalism
• Transitions (where m is a message, i & j are nodes)
– input send (m, i, j)
– output receive (m, i, j)
– input receiverListening (j)
– input receiverStopListening (j)
– input senderOpen (i, j)
– output respReceiverListening (i, j)
– input senderClose (i, j)
– internal senderClosing (i, j)
– input receiverClose (i, j)
– internal lose (m)
8
Implementation
• Distributed Abstract Channel functionality among
nodes
• Developed a Composite Channel with three types
of component automata
– JVM-TCP Channel
– Sender Mediator
– Receiver Mediator
• Based on Josh Tauber’s IOA compiler for a
Java/MPI interface
9
Node Automaton
Node i
Send
Mediator
Application
Automaton
Receive
Mediator
TCP
Sockets
JVMTCP
Channel
TCP
Sockets
10
Main Result
• Theorem: Composite Channel implements
Abstract Channel
The set of traces of Composite Channel is a subset of
the set of traces of Abstract Channel
• Proved using forward simulation
– Established a simulation relation mapping the states
of Composite Channel to the states of Abstract
Channel
– Showed the mapping holds for the initial states of
each automaton and is maintained by every transition
of Composite Channel
11
Summary
• First formal specification and implementation of an
abstract asynchronous communication channel with
explicit support for dynamic creation and teardown
of communication links
– Provides a building block for modeling dynamic
distributed applications and systems
– Serves as an aid to automated code generation
• Future Work (supported by an NSF grant)
– Bi-directional channels
– Multiple concurrent channels between node pairs
12
Thank You
13