Evolutionary Development of Complex Systems using Rapide: Transaction Processing Case Study, Atomicity

by Dr. John J. Kenney

last revised 98/7/10

Introduction

This document is an extension to the introductory example.  It continues in an evolutionary, example-driven style.  Again, this example is taken from my Ph.D. dissertation on transaction processing.  This document presents the models that specify atomicity.  Successive models present the properties of isolation and durability.  The models conclude with advanced features of security, distribution and performance.

Atomicity is a critical property of transaction processing systems. Atomicity is based upon the notion of grouping primitive actions to form larger, atomic transactions.  Primitive actions are assumed to have behaviors that are not decomposable, i.e., atomic.   Atomic operations are operations that are performed entirely or not at all; they cannot be only partially done at termination. Thus, transactions are not guaranteed to execute to completion, but instead are assured to be performed entirely or not at all.

System Model

We model a primitive action as a request-result pair of events. A group of primitive actions that forms a transaction is recognized by having all of its constituent request and result events share an unique identifier, called a transaction identifier or xid.

Also, the service that is shared among the application program and the resources has to be enriched to not only allow the application to make requests of the resources, but also instruct them whether they should commit the performance of the request or to undo the performance, called rollback.

Atomicity can be expressed via the following constraint: 

never (?x : Xid; ?rm1, ?rm2 : Resource_Manager)
    ?rm1.Commit_retn(?x,ok) ~ ?rm2.Rollback_retn(?x,ok);
Which means: A transaction, ?x, should never be committed by one resource, ?rm1, and rolled back by another resource, ?rm2.

Implementation System Architecture

Implementations of TP systems that satisfy the atomicity property generally have the following software architecture:
[Architecture]

In particular, the control logic for coordinating the resources to implement the atomicity property are abstracted into a transaction manager component. This saves each application program from having to implement the control logic. 

architecture System_A(NumRMs : Integer) is
  AP_A  : Application_Program_A(NumRMs);
  TM_A  : Transaction_Manager_A(NumRMs);
  RMs_A : Resource_Managers_A(NumRMs)
            is Some_RMs_A(NumRMs);
connect
  AP_A.TM ||> TM_A.AP;
  for i : Integer in 1..NumRMs generate
    AP_A.RMs(i) ||> RMs_A.RMs(i).AP;
    TM_A.RMs(i) ||> RMs_A.RMs(i).TM;
  end generate;
end architecture System_A;

System Components

Application Program 

type Application_Program_A(NumRMs : Integer) is
  interface
    service (1)
      RMs(1..NumRMs) : dual AP_RM_A;
      TM : dual AP_TM_A;
  behavior
    action (1)
      Continue(),
      Parallel_Requests(x : Xid),
      Single_Request(x : Xid; i : Integer);
    bool : var Boolean; 
    str : var String; 
  begin
   /*
After a Start or Continue event, decide what requests to perform and ask the TM for an xid. 
   */
    Start or Continue =>
      IO.Cput("Which resource to use?  [-1] quit, [0] all in parallel");
      str := IO.Cget();
      bool := Is_Image(Integer, $str);
      while ( not $bool ) do
        IO.Cput($str & " is not an integer, enter an integer.");
        str := IO.Cget();
        bool := Is_Image(Integer, $str);
      end do;
      if ( Value(Integer, $str) >= 0 ) then
        TM.Begin_call();
      end if;;

   /*
After getting an xid, decide to quit or generate either a single resource request or requests to all resources in parallel. 
   */
    (?x : Xid) TM.Begin_retn(?x, ok) =>
      if ( Value(Integer, $str) = 0 ) then
        Parallel_Requests(?x);
      elsif ( Value(Integer, $str) > 0 ) then
        Single_Request(?x, Value(Integer, $str) );
      end if;;

   /*
After making the decision generate a single resource request. 
   */
    (?x : Xid; ?i : Integer) Single_Request(?x, ?i) ||> (1)
      RMs(?i).Request(?x);;

   /*
After making the decision generate a request to each (1 to NumRMs) of the resources in parallel. 
   */
    (?x : Xid) Parallel_Requests(?x) ||> (1)
      [!i in 1..NumRMs rel ||] RMs(!i).Request(?x);;

   /*
If the AP made a single request and received a result back or if the AP made parallel requests and received NumRMs results back, then continue. 
   */
    (?x : Xid) (1)
    (( (?i : Integer) Single_Request(?x, ?i)
       ~ RMs(?i).Results(?x))
     or 
     ( Parallel_Requests(?x)
       ~ [!i in 1..NumRMs rel ~] RMs(!i).Results(?x) ))
    ||>
      TM.Commit_call(?x);;

    TM.Commit_retn ||> Continue();;
end interface Application_Program_A;

Resource Managers

Resource_Managers_A Type Constructor
type Resource_Managers_A(NumRMs : Integer) is
  interface
    service
      RMs(1..NumRMs) : Resource_Manager_A;
end interface Resource_Managers_A;
Resource_Manager_A Type Constructor 
type Resource_Manager_A is
  interface
    service
      AP : AP_RM_A;
      TM : TM_RM_A;
  behavior
  begin
    (?x : Xid) AP.Request(?x) ||> AP.Results(?x);;
    (?x : Xid) TM.Prepare_call(?x) ||> TM.Prepare_retn(?x, ok);;
    (?x : Xid) TM.Commit_call(?x) ||> TM.Commit_retn(?x, ok);;
    (?x : Xid) TM.Rollback_call(?x) ||> TM.Rollback_retn(?x, ok);;
end interface Resource_Manager_A;
Some_RMs Architecture 
architecture Some_RMs_A(NumRMs : Integer)
  return Resource_Managers_A(NumRMs) is
    RM_array : array[Integer] of Resource_Manager_A
                is (1..NumRMs, default is new(Resource_Manager_A));
  connect
    for i : Integer in 1..NumRMs generate
      RMs(i).AP ||> RM_array[i].AP;(1)
      RMs(i).TM ||> RM_array[i].TM;(1)
    end generate;
end architecture Some_RMs_A;

Transaction Manager

type Transaction_Manager_A(NumRMS : Integer) is
  interface
    service
      AP : AP_TM_A;
      RMs(1..NumRMs) : dual TM_RM_A;
  constraint
    never (?a, ?b : Integer; ?x : Xid) (1)
          RMs(?a).Commit_retn(?x, ok)
          ~ RMs(?b).Rollback_retn(?x, ok);

    never (?a, ?b : Integer; ?x : Xid; ?r : Return_Code) (1)
          RMs(?a).Prepare_retn(?x, ?r)
          || RMs(?b).Commit_call(?x);
  behavior
    Num : Integer is 3;  // Used to break the implmentation
    last_xid : var Xid := 0; 
    function New_Xid_t() return Xid is
    begin
      last_xid := $last_xid + 1;
      return $last_xid;
    end function New_Xid_t;
    x   : var Xid;
  begin 
    AP.Begin_call() ||>
      x := New_Xid_t();
      AP.Begin_retn($x, ok);;

    (?x : Xid)
    AP.Commit_call(?x) ||>
      [!i in 1..NumRMs rel ||] RMs(!i).Prepare_call(?x);;

    (?x : Xid) (1)
    [!i in 1..Num rel ~] RMs(!i).Prepare_retn(?x, ok)
    ||>
      [!i in 1..NumRMs rel ||] RMs(!i).Commit_call(?x);;

    (?x : Xid) (1)
    ( ( (?j : Integer) RMs(?j).Prepare_retn(?x, error) ) union 
      ( [!i in 1..Num rel ~] 
        ((?r : Return_Code) RMs(!i).Prepare_retn(?x, ?r)) ) )
    ||>
      [!i in 1..NumRMs rel ||] RMs(!i).Rollback_call(?x);;

    (?x : Xid) (1)
    [!i in 1..NumRMs rel ~]( RMs(!i).Commit_retn(?x, ok) )
    ||>
      AP.Commit_retn(?x, ok);;

    (?x : Xid) (1)
    [!i in 1..NumRMs rel ~]( RMs(!i).Rollback_retn(?x, ok) )
    ||>
      AP.Rollback_retn(?x, ok);;
end interface Transaction_Manager_A;

Services

AP_RM_A Interface Type (Service) 
type AP_RM_A is
  interface
    action
      in  Request(x : Xid); (1)
      out Results(x : Xid); (1)
end interface AP_RM_A;
AP_TM_A Interface Type (Service) 
type AP_TM_A is
  interface
    action
      in  Begin_call   ();
      out Begin_retn   (x : Xid; rc : Return_Code);
      in  Commit_call  (x : Xid);
      out Commit_retn  (x : Xid; rc : Return_Code);
      in  Rollback_call(x : Xid);
      out Rollback_retn(x : Xid; rc : Return_Code);
end interface AP_TM_A;
TM_RM_A Interface Type (Service) 
type TM_RM_A is
  interface
    action
      in  Prepare_call(x : Xid);
      out Prepare_retn (x : Xid; rc : Return_Code); (1)
      in  Commit_call(x : Xid); (1)
      out Commit_retn  (x : Xid; rc : Return_Code); (1)
      in  Rollback_call(x : Xid);
      out Rollback_retn(x : Xid; rc : Return_Code); (1)
end interface TM_RM_A;

Basic Types

Transaction Identifier Type
type Xid is Integer;
Returned Code Type
type Return_Code is enum ok, error end enum Return_Code;

Map from Atomcity to Fundamental Concepts 

map Map_A_to_FC(N : Integer)
  from D : System_A
  to System_FC_nb(N)
  is
  rule
    D.AP_A.Continue ||> AP_FC.Continue();;

    D.AP_A.Parallel_Requests ||> AP_FC.Parallel_Requests();;

    (?x : Xid; ?i : Integer)
    D.AP_A.Single_Request(?x, ?i)
    ||> 
      AP_FC.Single_Request(?i);;

    (?i : Integer; ?x : Xid)
    D.AP_A.RMs(?i).Request(?x, ?i)
    ||> 
      AP_FC.Rsrcs(?i).Request();;

    (?i : Integer; ?x : Xid)
    D.RMs_A.RMs(?i).AP.Request(?x, ?i)
    ||> 
      Rs_FC.Rsrcs(?i).AP.Request();;

    (?i : Integer; ?x : Xid)
    Resource_Manager_A::AP.Results(?x, ?i)
    ||> 
      Rs_FC.Rsrcs(?i).AP.Results(performer is Rs_FC.Rsrcs(?i));;

    (?i : Integer; ?x : Xid)
    D.RMs_A.RMs(?i).AP.Results(?x, ?i)
    ||> 
      Rs_FC.Rsrcs(?i).AP.Results();;

    (?i : Integer; ?x : Xid)
    D.AP_A.RMs(?i).Results(?x, ?i)
    ||> 
      AP_FC.Rsrcs(?i).Results();;

end map Map_A_to_FC;

System Execution(s)

Main_A Module

architecture Main_A() is
    N : Integer is String_To_Integer(Arguments[1]);
    S : Root is System_A(N);
    M is map Map_A_to_FC(N, S);
connect
end architecture Main_A;

The previous architectural description is executable, and upon execution the following history was produced. This history reflects the user's choice of performing a single request, parallel requests, and then another single request.

[Execution]

System Animation

Running the animation is not available via html. The architecture file for the animation is here .

Footnotes

(1)

The Rapide 1.0 compiler is limited to performing only a limited form of dynamic subtype checking and pattern matching. These limitations are signification in the application program here and in the map here.

A workaround for these bugs require the following additional action definitions placed here. 

action
  in Continue(), 
     Parallel_Requests(x : Xid), 
     Single_Request(x : Xid; i : Integer);
and the removal of the corresponding action definitions in the behavior here.

A workaround for this bug requires the behavioral rule placed here to be replaced with: 

(?x : Xid; ?i : Integer) Single_Request(?x, ?i) ||>
  RMs(?i).Request(?x, ?i);;

and a similar replacement here to be replaced with: 

(?x : Xid) Parallel_Requests(?x) ||>
  [!i in 1..NumRMs rel ||] RMs(!i).Request(?x, !i);;

and a similar replacement here to be replaced with:

(?x : Xid)
(( (?i : Integer) Single_Request(?x, ?i)
   ~ RMs(?i).Results(?x, ?i) )
 or
 ( Parallel_Requests(?x)
   ~ [!i in 1..NumRMs rel ~] RMs(!i).Results(?x, !i) ))
||>
  TM.Commit_call(?x);;

A workaround for this bug requires this additional connection rules placed here: 

(?x : Xid)
RMs(i).AP.Request(?x)
  ||> RM_array[i].AP.Request(?x);

(?x : Xid)
RM_array[i].AP.Results(?x)
  ||> RMs(i).AP.Results(?x, i);

A workaround for this bug requires this additional connection rules placed here: 

(?x : Xid)
RMs(i).TM.Prepare_call(?x)
  ||> RM_array[i].TM.Prepare_call(?x);

(?x : Xid; ?c : Return_Code)
RM_array[i].TM.Prepare_retn(?x, ?c)
  ||> RMs(i).TM.Prepare_retn(?x, ?c, i);

(?x : Xid)
RMs(i).TM.Commit_call(?x)
  ||> RM_array[i].TM.Commit_call(?x);

(?x : Xid; ?c : Return_Code)
RM_array[i].TM.Commit_retn(?x, ?c)
  ||> RMs(i).TM.Commit_retn(?x, ?c, i);

(?x : Xid)
RMs(i).TM.Rollback_call(?x)
  ||> RM_array[i].TM.Rollback_call(?x);

(?x : Xid; ?c : Return_Code)
RM_array[i].TM.Rollback_retn(?x, ?c)
  ||> RMs(i).TM.Rollback_retn(?x, ?c, i);

The workaround also requires the constraints defined here and here to be modified as follows: 

never (?a, ?b : Integer; ?x : Xid)
    RMs(?a).Commit_retn(?x, ok, ?a)
    ~ RMs(?b).Rollback_retn(?x, ok, ?b);

never (?a, ?b : Integer; ?x : Xid; ?r : Return_Code)
    RMs(?a).Prepare_retn(?x, ?r, ?a)
    || RMs(?b).Commit_call(?x, ?b);

The workaround also requires the rule defined here to be modified to: 

(?x : Xid)
[!i in 1..Num rel ~] RMs(!i).Prepare_retn(?x, ok, !i)
||>
  [!i in 1..NumRMs rel ||] RMs(!i).Commit_call(?x, !i);;

The workaround also requires the rule defined here to be modified to: 

(?x : Xid)
( ( (?j : Integer) RMs(?j).Prepare_retn(?x, error, ?j) ) union 
  ( [!i in 1..Num rel ~] 
    ((?r : Return_Code) RMs(!i).Prepare_retn(?x, ?r, !i)) ) )
||>
  [!i in 1..NumRMs rel ||] RMs(!i).Rollback_call(?x);;

The workaround also requires the rule defined here to be modified to: 

(?x : Xid)
[!i in 1..NumRMs rel ~]( RMs(!i).Commit_retn(?x, ok, !i) )
||>
  AP.Commit_retn(?x, ok);;

The workaround also requires the rule defined here to be modified to: 

(?x : Xid)
[!i in 1..NumRMs rel ~]( RMs(!i).Rollback_retn(?x, ok, !i) )
||>
  AP.Rollback_retn(?x, ok);;

As well as replacing the action declarations placed here and here with:

in  Request(x : Xid; i : Integer);
out Results(x : Xid; i : Integer);

As well as replacing the action declarations placed here, here, here, and here with:

out Prepare_retn (x : Xid; rc : Return_Code; i : Integer);
in  Commit_call(x : Xid; i : Integer);
out Commit_retn  (x : Xid; rc : Return_Code; i : Integer);
out Rollback_retn(x : Xid; rc : Return_Code; i : Integer);