Consistency for
Web Services Applications
Paul Greenfield
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Web Service Vision

Internet-scale distributed applications

Composed from autonomous & opaque ‘services’





Platform and language agnostic
Limited trust between participants




Custom code, packages, partners (Amazon, DHL, …)
Service behaviour/expectations ideally defined by contracts
Services often stateful with multiple related interactions
Running over public networks?
Services open to all (authenticated?) callers?
No direct access to internal state
Nice vision, but will prove hard to realise


All the old distributed computing problems still around
Inconsistent outcomes & other errors quite likely…
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Why Are Services Different?

Autonomous



Opaque



Participants can behave as they wish…
…as long as they comply with their contract
Cannot assume central coordinator or controller
Only know about contracts & defined behaviour
Cannot look inside services to determine their state
Limited trust


Would you trust callers to release locks?
Makes traditional distributed transactions infeasible
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
eProcurement Example

Multi-step stateful customer-merchant dialogue

Normal case simple; complexities come from
application exceptions, asynchronicity & concurrency
quote request
quote
purchase order
confirmation
Customer
Service
invoice
Merchant
Service
payment
receipt
goods shipped
goods received
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
What Could Go Wrong?
All participating services must always reach
agreed consistent outcomes
 Failure to terminate (deadlocks, starvation, …)


Unprocessed messages left after termination


Merchant & customer waiting for each other
Payment reminder after customer terminated
Inconsistent outcomes




Services must finish in globally consistent states
Customer must reflect merchant’s state & vice versa
…both think payment has been made or not…
Problem long solved by transactions…
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Consistency & Transactions

Traditional distributed transaction problem


Already solved by X-Open, CICS, …
What about WS transaction standards?

WS-AT assumes trust and timeliness




WS-BA termination protocol only



Conventional ACID transactions with 2-phase commit
Good support for consistency and isolation
Limited applicability in open services world
Coordinating termination, possibly invoking compensators
Doesn’t really address consistency or isolation
BTP, WS-CAF, …

Patterns and related protocols only
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Inconsistent Outcomes

How could a distributed application finish with
its participating services in inconsistent states?

How can the merchant and customer disagree?


What exchange of messages lead to this outcome?




Paid and not paid, goods delivered and goods not received
Messages rejected or unprocessed?
Incompatibility between customer & merchant processes?
Protocol errors and faulty designs
Introduces ‘correctness’ & ‘compatibility’

Being able to reach inconsistent outcomes is a
design fault...
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Our Approach

Tools, programming models, patterns

Detect correctness/consistency faults at design time




Test for compatibility between services
Detect consistency faults at run time
Patterns for defining correct application protocols
Using relationship between states & messages



Transform consistency into protocol correctness
Use protocol verification tools to detect inconsistent
outcomes and other errors at design time
Basis of run time checking protocol as well
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Consistency, States & Messages

Set of participating services must finish in one of
an agreed set of consistent distributed ‘states’


(payment sent & payment received and goods
received & goods sent) or …
Specified using global constraint expressions?

Expressions over internal service state?




Not possible given opaque nature of services
Not possible for external coordinator to observe states
All we know is what messages have been sent/received
Try expressions over messaging history…
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Messaging History and States

All internal state that needs to be referenced in
consistency expressions will be unambiguously
reflected in protocol messages




Occurrence of message is proxy for state change


‘Payment complete’  receipt message
We assert this is true for significant no. of applications
Just reflects normal business practices
Allows consistency expressions referring only to
messages exchanged between participants
Lets us transform consistency problem into
protocol correctness problem…

So we need to look at protocols…
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Contracts and Protocols

Application protocol



Set of all possible message sequences that can be
exchanged between participating services
Results from interactions between contracts…
Contract




Abstract definition of externally observable
messaging behaviour of a service
Specify messages that can be sent and received
Specify causal relationship between these messages
(extension) Specify local acceptable consistency
constraints at termination
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Contracts

Needed simple & expressive contract language

Defined condition-based contracts language


Concise & expressive way to specify behaviour




Similar to ECA programming languages
Especially when asynchronous messages allowed
More concise than BPEL4WS, CSP, …
Specify messages each service can send or receive
Conditions state when messages can be sent or
received
Send: invoice
Condition: sent purchase order confirmation and
not sent cancel accept
Receive: payment
Condition: sent invoice and not sent cancel accept

Used in SSDL Rules protocol framework
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Contracts and Protocols

Given 2 contracts we can derive (enumerate)
the corresponding application protocol

Just the set of all possible message sequences
quote request, quote, purchase order,
order confirmation, invoice, payment
quote request, quote, purchase order,
request, purchase order confirmation,
reject, invoice, payment
quote request, quote, purchase order,
request, cancellation accept
… … …

purchase
cancellation
cancellation
cancellation
Asynchronous messages commonly needed

Add complexity to protocol & application design


Timeouts, exceptions, cancellation, …
… Add the possibility of races, deadlocks, …


Sending late fee while payment in transit
Could result in inconsistent outcomes
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Static Consistency Checking

Design-time tools for finding errors



Define contracts of participating services
Generate application protocol message sequences
Check that all sequences meet correctness criteria





Always terminate
No unprocessed messages at termination
Message-based consistency constraints always hold
Find and fix contract errors that result in failures
Proof-of-concept built using SPIN




Model-checker used for protocol verification
Contracts specified in PROMELA
Global consistency constraints in LTL
Constraints and contracts written by hand
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Model Checking

SPIN generates all possible message sequences



Including all allowable orderings
Some messages marked as ‘final’
SPIN checks …




All messages compatible with contracts
No messages left unprocessed at termination
All sequences result in termination
And… global consistency constraints satisfied


Referring only to messages sent or received
Agreement on delivery and payment



Merchant sent receipt & received goods received
Customer received receipt & sent goods received
Many alternative acceptable outcomes possible
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Service Compatibility

Or… checking if 2 services are ‘compatible’

All possible interactions lead to correct outcomes




Not all messages have to be used…


Customer and merchant interactions will always terminate &
reach consistent outcomes…
Both sides always only send ‘acceptable’ messages
Is my client compatible with Amazon’s service?
Merchant may support more payment types than customer
Contracts can support negotiation

Cancellation allowed, payments accepted, …
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Tool Development

Correctness checking from SSDL Rules

Extend SSDL Rules with local consistency constraints




Generate PROMELA & LTL definitions
Run contract compatibility/correctness check
Generate SSDL rules from program definition



Assuming global constraints can be derived from local
constraints
Event-based programming model (GAT)
Also generate C# code from GAT description
Extending SSDL rules to invoke WS-BA
termination paths
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Protocol Design

Designing error-free contracts proved hard


Use of WS-BusinessActivity helped



Race conditions and unprocessed messages
Standard toolkit of termination protocol paths
Resolved many termination-related problems
State must always be reflected in messages

Changes to merchant’s ‘paid’ state always signalled


Must be unambiguous


Merchant reaches ‘paid’ state  receipt message sent
Receipt message can only mean merchant is ‘paid’
Just reflects traditional business processes…
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
On-going Work

Run-time consistency checking

Protocol to check consistency at termination


Check for local consistency and ask neighbours



Reflected state links participants
No need for global constraints and coordinator
Isolation patterns and protocols


Static checking just proves presence of design flaws
Looking into pattern-based solutions to isolation
More formal correctness proofs



Multi-party extensions
Use of local consistency constraints
Validity of state-message assertion…
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Summary

Consistency, correctness and compatibility


Impediments hindering the Web Services vision
Tool-based approach to finding design flaws



Consistency-related state signalled by messages
Consistency constraints can refer only to messages
Allows use of protocol verification tools



Check for correctness, including consistent outcomes
Proof-of-concept and follow-on tools produced
Working on dynamic checking protocol

Based on local consistency and reflected state
The CeNTIE project is supported by the Australian Government through the Advanced Networks Program
of the Department of Communications, Information Technology and the Arts.
Descargar

Distributed Systems Research