Theoretical Foundations for
Compensations in Flow
Composition Languages
Hernán Melgratti
Joint work with Roberto Bruni and Ugo Montanari
Dipartimento di Informatica - Università di Pisa
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Motivations: Web Service Composition
Defining complex services as aggregations of
simpler services
Interaction based Composition, Conversational
Patterns or Global Model
Services describe the ways they can be engaged in a
larger process
Flow Composition or Hierarchical Patterns
Similar to workflow systems: a process describes the
flow of both control and data among WS
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Motivations: Flow Composition
A2
A1
A3
A5
A4
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Motivations: Transactional Flow
Transactional Process
A2
A1
A3
A5
A4
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Motivations: Compensation
Transactional Process
A1
B1
A2
A3
B2
B3
A4
A5
B5
B4
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Motivations: Compensation Flow
Transactional Process
A1
B1
A2
A3
B2
B3
A4
A5
B5
B4
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Outline of the talk
Sequential Sagas
Graphical representation
Syntax and Semantics
Adequacy results
Parallel Sagas
Nested Sagas
Additional features
Concluding remarks
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Graphical Repr.
Accept Order
Update Credit
Prepare Order
Refuse Order
Refund Money
Update Stock
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Syntax
Accept Order
Update Credit
Prepare Order
Refuse Order
Refund Money
Update Stock
(Step)
X ::= 0 | A | A%B
(Process) P ::= X | P;P
(Saga)
S ::= { P }
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Syntax
Accept Order
Update Credit
Prepare Order
Refuse Order
Refund Money
Update Stock
S = { AO%RO ; UC%RM ; PO%US }
(Step)
X ::= 0 | A | A%B
(Process) P ::= X | P;P
(Saga)
S ::= { P }
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Semantics
An activity A either
commits (A  )
aborts (A  )
 = {A1  ,…, An  }
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Semantics
A saga S = { P } under  either


commits (  S  )

aborts (  S  )


fails ( 

S  * )
 is the observable flow
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Semantics
A process P under  either

 < ,ß’> )
commits (  <P,ß> 
 < , 0> )
aborts (  <P,ß> 
 < , 0> )
fails (  <P,ß> 
*


ß and ß’ are the installed compensations
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Semantics

(saga)



<P,0>  < , ß>

 {P} 
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Semantics


<P,0>  < , ß>

 {P} 

(zero)

(saga)


Hernán Melgratti
0 < , ß>
<0,ß> 
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Semantics


<P,0>  < , ß>

 {P} 

(zero)

(saga)


A ,
Hernán Melgratti

(s-act)
0 < , ß>
<0,ß> 
A < , B;ß>
<A%B, ß> 
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Semantics


<P,0>  < , ß>

 {P} 

(zero)

(saga)


A ,

(s-act)
0 < , ß>
<0,ß> 
A < , B;ß>
<A%B, ß> 
(f-cmp)

<ß,0>  < , 0>
 < , 0>
A  ,  <A%B,ß> 
*

(s-cmp)

<ß,0>  < , 0>
 < , 0>
A  ,  <A%B,ß> 





Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Semantics


Hernán Melgratti

<P,ß>  < , 0>

<P;Q,ß>  < ,0>

<P,ß>  < * , 0>

<P;Q,ß>  < * ,0>
 
(a-step’’)







(a-step’)
’
 <Q,ß’’>  < ,ß’>
;’
<P;Q, ß>  < ,ß’>

<P,ß>  < ,ß’’>

(s-step)

POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Adequacy Theorem

S 


A1
Hernán Melgratti
and = A1;…;An
Aj
Ak
An
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Adequacy Theorem
Hernán Melgratti
and = A1;…;An
Ak
A1
Aj

S 
and = A1;…;Ak-1;Bk-1;…;B1
A1
Aj
B1
Bj



S 


Ak
An
An
POPL2005, Long Beach, Jan.12-14, 2005
Sequential Sagas: Adequacy Theorem
Hernán Melgratti
Ak
Aj

S 
and = A1;…;Ak-1;Bk-1;…;B1
A1
Aj
B1
Bj
Ak
An
An

S  * and = A1;…;Ak-1;Bk-1;…;Bj+1


and = A1;…;An
A1



S 


A1
Aj
B1
Bj
Ak
An
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Graphical Representation
Update Credit
Accept Order
Refuse Order
Refund Money
Prepare Order
Update Stock
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Syntax
Update Credit
Accept Order
Refuse Order
Refund Money
Prepare Order
Update Stock
(Step)
X ::= 0 | A | A%B
(Process) P ::= X | P;P | P|P
(Saga)
S ::= { P }
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Syntax
Update Credit
Accept Order
Refuse Order
Refund Money
Prepare Order
Update Stock
S = { AO%RO ; UC%RM | PO%US }
(Step)
X ::= 0 | A | A%B
(Process) P ::= X | P;P | P|P
(Saga)
S ::= { P }
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: The Naïve Way
A1
A’1
B1
Bj
B’1
B’j
Bn
A2
C1
Ck
Cm
C’1
C’k
C’m
A1;(B1;…;Bj-1;B’j-1;…;B’1 | C1;…Cm;C’m;…;C’1);A’1
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Revised
A1
A’1
B1
Bj
B’1
B’j
Bn
A2
C1
Ck
Cm
C’1
C’k
C’m
A1;(B1;…;Bj-1;B’j-1;…;B’1 | 0);A’1
A1;(B1;…;Bj-1;B’j-1;…;B’1 | C1;C’1);A’1
…
A1;(B1;…;Bj-1;B’j-1;…;B’1 | C1;…Cm;C’m;…;C’1);A’1
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Semantics
A process P under  either

 < ,ß’> )
commits (  <P,ß> 
 < , 0> )
aborts (  <P,ß> 
 < , 0> )
fails (  <P,ß> 
*
 < , 0> )
is forced to abort (  <P,ß> 
 < , 0> )
is forced to fail (  <P,ß> 
*




 is the observable concurrent flow
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Semantics

<P,0>  <, ß>

 {P}  

(saga)

{
,
, *}




<ß, 0>  < , 0>

<P,ß>  < * ,0>


Hernán Melgratti


(forced-abt’’)

<ß, 0>  < , 0>

<P,ß>  < ,0>

(forced-abt’)

POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Semantics
Hernán Melgratti



’
<Q,0>  < ,ß’’>


<P,0>  < ,ß’>

(s-par)

|’
<P|Q, ß>  < ,ß’|ß’’; ß>
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Semantics
(c-par’)
 1,  2  {

<ß,0>  < ,0>


}
|’; 
<P|Q, ß>  < 1  2 , 0>


’
 <Q,0>  <2,0>



 <P,0>  <1,0>
,

*
*

*

*

*
Hernán Melgratti

*
*
*
*
*
*
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Semantics
(c-par’’)
 1,  2  {

<ß,0>  < ,0>


}
|’; 
<P|Q, ß>  < 1  2  * , 0>


’
 <Q,0>  <2,0>



 <P,0>  <1,0>
,

*
*

*

*

*
Hernán Melgratti

*
*
*
*
*
*
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Semantics
(f-par)
|’
<P|Q, ß>  < 1  2 , 0>
1  { * , * }
2  {
,
, * , *}


’
 <Q,0>  <2,0>



 <P,0>  <1,0>

*
*

*

*

*
Hernán Melgratti

*
*
*
*
*
*
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Adequacy
Completion
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Adequacy
Successful Compensation
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Parallel Sagas: Adequacy
Failed Compensation
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Nested Sagas: Graphical Representation
Update Credit
Accept Order
Refuse Order
Refund Money
Prepare Order
Update Stock
Add Points
Subtract Points
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Nested Sagas: Syntax
(Step)
X
(Process) P
(Saga)
S
Hernán Melgratti
::= 0 | A | A%B | S
::= X | P;P | P|P
::= { P }
POPL2005, Long Beach, Jan.12-14, 2005
Nested Sagas: Syntax
Update Credit
Accept Order
Refuse Order
Refund Money
Prepare Order
Update Stock
Add Points
Subtract Points
S  { AO%RO ; UC%RM | PO%US | {AP%SP} }
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Nested Sagas: Semantics
(sub-cmt)



<P,0>  < , ß’>

<{P},ß>  < , ß’;ß>


ß’ acts as default compensation
(sub-abt)

Hernán Melgratti



<P,0>  < * , 0>

<{P},ß>  < * , 0>

(sub-fail)



<P,0>  < , 0>

<{P},ß>  < , ß>


POPL2005, Long Beach, Jan.12-14, 2005
Nested Sagas: Semantics
(sub-forced-1)



<P,0>  < * , 0>

<{P},ß>  < * , 0>


(sub-forced-2’)




 <ß,0>  < ,0>
;
<{P}, ß>  < ,0>

<P,0>  < ,0>


(sub-forced-2’’)



Hernán Melgratti

 <ß,0>  <,0>
;
<{P}, ß>  < * ,0>

<P,0>  < ,0>


{
,*}
POPL2005, Long Beach, Jan.12-14, 2005
Nested Sagas: Adequacy
Completion
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Nested Sagas: Adequacy
Successful Compensation
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Nested Sagas: Adequacy
Failed Compensation
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
More on Sagas
Exception handling try S with P
Used to catch crashes during backward computation
Forward recovery strategies try S or P
Can be used to retry or to improve activities
Fully programmable compensations S%P
More expressive than default compensation (sub-cmt)
Allowed by languages like BPEL4WS
Choices:
discriminator PQ
internal PQ
Data dependencies AB
Valid executions must satisfy dependency constraints
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Final Remarks
Our definition for compensable languages
abstracts away from low-level computations
can be easily extended
independent from the coordination mechanisms
that implement the primitives
Java Transactional Web Services (JTWS)
Distributed implementation of flows
Allows to reason about program properties
Adequacy
Correctness of implementation
Hernán Melgratti
POPL2005, Long Beach, Jan.12-14, 2005
Descargar

Implementing Transactions in JOIN Calculus