Copyright ©2008 T. H. Merrett
COMP 617 Information Systems Winter 2008 Week 3
Aborting in Aldat
Modified example from p.76 of [BernNewc:TP]: paying credit card bill(s).
CREDIT_CARD ACCOUNTS
(ACCT_NO AMOUNT) (ACCT_NO BALANCE)
1 $2 1 $10
3 $2 2 $10
4 $1 3 $ 1
4 $ 1
1. Batch payment (better for Aldat than for SQL).
(For simplicity, assume bank and credit card use same ACCT_NOs.)
update ACCOUNTS change BALANCE <- BALANCE - AMOUNT using CREDIT_CARD;
ACCOUNTS
(ACCT_NO BALANCE)
1 $ 8
2 $10
3 $-1
4 $ 0
update CREDIT_CARD change AMOUNT<- 0 using where BALANCE>=0 in ACCOUNTS;
CREDIT_CARD
(ACCT_NO AMOUNT)
1 $0
3 $2
4 $0
abort(where BALANCE < 0 in ACCOUNTS);
ACCOUNTS
(ACCT_NO BALANCE)
1 $ 8
2 $10
3 $ 1
4 $ 0
An equivalent to this abort would be by event handler
comp post:change:ACCOUNTS[BALANCE]() is
{ let BAL be BALANCE;
update ACCOUNTS change BALANCE <- BAL using
((where BALANCE < 0 in ACCOUNTS) ijoin [ACCT_NO,BAL] in .trigger)
};
but the abort is explicit and, we'll see, can be used to communicate.
Note that the abort is partial, rolling back only the data specified by the
predicate.
We probably need more explicit syntax than
abort(where BALANCE < 0 in ACCOUNTS)
to pick up that ACCOUNTS is the relation to be re-set.
2. Individual payment, following [BernNewc:TP]. Now we introduce transactions
(atomic: all or nothing, for system crashes (unlike abort, above);
durable: written immediately to persistent storage, for system crashes;
isolated: independent of concurrent transactions, for concurrency).
(We could spell out these properties explicitly and independently of each
other, but since we cannot anticipate either crashes or concurrent updates
to the same data, we always combine into the keyword transaction .)
Note that atomicity implies the ability of the system to abort a transaction,
i.e., roll it back in its entirety. Giving the user the ability to abort, as
we have already done, just anticipates this.
comp Pay_Bill(bankAcct,credCardAcct) is transaction
{ Pay_cc(in credCardAcct, out amount); << start transaction at { >>
Debit-b(in bankAcct, in amount);
if aborted(Debit_b) then abort
} << commit transaction at } >>
comp Pay_cc(credCardAcct,amount) is
{ amount <- << scalar: ACCT_NO is key >>
[red max of AMOUNT] where ACCT_NO=credCardAcct in CREDIT_CARD;
update CREDIT_CARD change AMOUNT <-
if ACCT_NO=credCardAcct then 0 else AMOUNT
}
comp Debit_b(bankAcct,amount) is
{ update ACCOUNTS change BALANCE <-
if ACCT_NO=bankAcct then BALANCE - amount else BALANCE;
abort(Debit_b, where BALANCE < 0 in ACCOUNTS)
}
Pay_Bill(in 3, in 3) will abort.
Pay_Bill(in 1, in 1) will commit.
Note that abort(Debit_b, where BALANCE < 0 in ACCOUNTS) just rolls back the
overdraft, if any. It does not abort the transaction. But comp Debit_b is
contained in a transaction, and the abort of the transaction is total.
Note that abort(Debit_b, ..) communicates with the predicate aborted(Debit_b)
We don't need to specify abort(Debit_b, - abort can pick this up from the
containing computation - but we specify it anyway for clarity.
Aborted should be able to return .trigger (which should be trigger()!)
as a parameter.
Note that any statement may be labelled a transaction (redundant because
Aldat statements are individually atomic and isolated), and any bracketed
group of statements may be labelled a transaction: transaction{..}.
(Only the body of a computation has a name, in case we want to communicate
what aborted.)
P.S. Any computation invoked directly or indirectly from within a transaction
is part of the transaction. This includes event handlers in particular.
3. Nested transactions (pp.318--22 of [BernNewc:TP])
Motivation:
1. Encapsulation: if a computation is already a transaction and we invoke it
from within another transaction, this should have meaning.
2. Remote processing might be more efficient using transactions (within
another transaction): preceding an update by a test might cost two
Internet interactions, while a transaction with the option of aborting
can be done in one.
3. It may be desirable to refine the granularity of locking (against
concurrent updates): e.g., for high concurrency, or for long-duration
transactions (pp.116--21 of [BernNewc:TP]). At the risk of losing
isolation. (Atomicity can be preserved by specifying "compensating
transactions" which undo earlier transactions should a later transaction
fail or abort.)
comp Pay_Bill(bankAcct,credCardAcct) is transaction
{ Pay_cc(in credCardAcct, out amount); << start transaction at { >>
Debit-B(in bankAcct, in amount);
if aborted(Debit_b) then abort
} << commit transaction at } >>
comp Pay_cc(credCardAcct,amount) is transaction
{ amount <- << scalar: ACCT_NO is key >>
[red max of AMOUNT] where ACCT_NO=credCardAcct in CREDIT_CARD;
update CREDIT_CARD change AMOUNT <-
if ACCT_NO=credCardAcct then 0 else AMOUNT
}
comp Debit_b(bankAcct,amount) is transaction
{ update ACCOUNTS change BALANCE <-
if ACCT_NO=bankAcct then BALANCE - amount else BALANCE;
if [] where BALANCE < 0 in ACCOUNTS then abort(Debit_b)
}
Now abort(Debit_b) must abort the whole subtransaction (which it did before
anyway, since ACCT_NO is a key, but didn't need to).
The rules have changed: subtransactions are not durable, and their changes
are visible to the parent transaction, but not beyond, nor to sibling
subtransactions. The system implementing transactions must recognize
whether or not it is seeing a top-level transaction or a subtransaction.
4. A more convincing use of nested transactions (p.320 of [BernNewc:TP]):
privileged bank customers with overdraft protection.
CREDIT_CARD ACCOUNTS OVERDRAFT_ALLOWED
(ACCT_NO AMOUNT) (ACCT_NO BALANCE) (ACCT_NO LIMIT CURRENT)
1 $2 1 $10 3 $5 $0
3 $2 2 $10
4 $1 3 $ 1
4 $ 1
comp Pay_Bill(bankAcct,credCardAcct) is transaction
{ Pay_cc(in credCardAcct, out amount); << start transaction at { >>
Debit-B(in bankAcct, in amount);
if aborted(Debit_b) then
{ Zero-B(in bankAcct, out amount);
Overdraw_b(in bankAcct,in amount);
}
if aborted(Overdraw_b) then abort
} << commit transaction at } >>
comp Pay_cc(credCardAcct,amount) is transaction
{ amount <- << scalar: ACCT_NO is key >>
[red max of AMOUNT] where ACCT_NO=credCardAcct in CREDIT_CARD;
update CREDIT_CARD change AMOUNT <-
if ACCT_NO=credCardAcct then 0 else AMOUNT
}
comp Debit_b(bankAcct,amount) is transaction
{ update ACCOUNTS change BALANCE <-
if ACCT_NO=bankAcct then BALANCE - amount else BALANCE;
if [] where BALANCE < 0 in ACCOUNTS then abort(Debit_b)
}
comp Zero-b(bankAcct,amount) is transaction
{ amount <- [red max of amount - BALANCE]
where ACCT_NO = bankAcct in AMOUNTS;
update ACCOUNTS change BALANCE <-
if ACCT_NO=bankAcct then 0 else BALANCE;
}
comp Overdraw_b(bankAcct,amount) is transaction
{ update OVERDRAFT_ALLOWED change CURRENT <-
if ACCT_NO=bankAcct then CURRENT + amount else CURRENT;
if [] where CURRENT > LIMIT in OVERDRAFT_ALLOWED then abort(Overdraw_b)
}
Pay_Bill(in 3, in 3) will now commit.
5. If the various component transactions were run on different hosts, using the
abort mechanism needs only one remote invocation. The alternative would be
to test the balance in the account (one invocation) then decide to withdraw
(a second invocation), or to test the overdraft limit then decide to overdraw
(again two invocations). (Note that the test and withdrawal must be within a
transaction or else some other process might withdraw the money between the
test and our withdrawal.)
Suppose CREDIT_CARD is on host C, ACCOUNTS and OVERDRAFT_ALLOWED are on
host B, and the top level Pay_Bill transaction is running on a third,
unnamed, host.
comp Pay_Bill(bankAcct,credCardAcct) is transaction
{ aldat_p:/C/Pay_cc(in credCardAcct, out amount); <>
aldat_p:/B/Debit-b(in bankAcct, in amount);
if aborted(Debit_b) then
{ aldat_p:/B/Zero-B(in bankAcct, out amount);
aldat_p:/B/Overdraw_b(in bankAcct,in amount);
}
if aborted(Overdraw_b) then abort
} << commit transaction at } >>
<< On host C: >>
comp Pay_cc(credCardAcct,amount) is transaction
{ amount <- << scalar: ACCT_NO is key >>
[red max of AMOUNT] where ACCT_NO=credCardAcct in CREDIT_CARD;
update CREDIT_CARD change AMOUNT <-
if ACCT_NO=credCardAcct then 0 else AMOUNT
}
<< On host B: >>
comp Debit_b(bankAcct,amount) is transaction
{ update ACCOUNTS change BALANCE <-
if ACCT_NO=bankAcct then BALANCE - amount else BALANCE;
if [] where BALANCE < 0 in ACCOUNTS then abort(Debit_b)
}
comp Zero-b(bankAcct,amount) is transaction
{ amount <- [red max of amount - BALANCE]
where ACCT_NO = bankAcct in AMOUNTS;
update ACCOUNTS change BALANCE <-
if ACCT_NO=bankAcct then 0 else BALANCE;
}
comp Overdraw_b(bankAcct,amount) is transaction
{ update OVERDRAFT_ALLOWED change CURRENT <-
if ACCT_NO=bankAcct then CURRENT + amount else CURRENT;
if [] where CURRENT > LIMIT in OVERDRAFT_ALLOWED then abort(Overdraw_b)
}
6. The code is still a single transaction and will not allow concurrent access
to the relations (or to the pertinent tuples of the relations, depending on
the granularity of the locking used to enforce isolation) by other processes.
At the risk of losing isolation we can increase concurrency by removing the
outer transaction to have a sequence of independent, top-level transactions.
We can somewhat preserve atomicity by specifying compensating transactions.
(But concurrent transactions can see the intermediate results, which might
even make the database inconsistent, because top-level transactions are
durable.) The result is called a "saga".
comp Pay_Bill(bankAcct,credCardAcct) is
{ Pay_cc(in credCardAcct, out amount);
Debit-B(in bankAcct, in amount);
if aborted(Debit_b) then
{ Zero-B(in bankAcct, out amount);
Overdraw_b(in bankAcct,in amount);
}
if aborted(Overdraw_b) then << complain! >>
}
comp Pay_cc(credCardAcct,amount) is transaction
{ amount <- << scalar: ACCT_NO is key >>
[red max of AMOUNT] where ACCT_NO=credCardAcct in CREDIT_CARD;
update CREDIT_CARD change AMOUNT <-
if ACCT_NO=credCardAcct then 0 else AMOUNT
} compensated by transaction
{ update CREDIT_CARD change AMOUNT <-
if ACCT_NO=credCardAcct then amount else AMOUNT
<< will it remember changed amount? >>
}
comp Debit_b(bankAcct,amount) is transaction
{ update ACCOUNTS change BALANCE <-
if ACCT_NO=bankAcct then BALANCE - amount else BALANCE;
if [] where BALANCE < 0 in ACCOUNTS then abort(Debit_b)
} compensated by transaction
{ update ACCOUNTS change BALANCE <-
if ACCT_NO=bankAcct then BALANCE + amount else BALANCE
}
comp Zero-b(bankAcct,amount) is transaction
{ amount <- [red max of amount - BALANCE]
where ACCT_NO = bankAcct in AMOUNTS;
update ACCOUNTS change BALANCE <-
if ACCT_NO=bankAcct then 0 else BALANCE;
} compensated by transaction
{ update ACCOUNTS change BALANCE <-
if ACCT_NO=bankAcct then amount else BALANCE
<< will it remember changed amount? >>
}
comp Overdraw_b(bankAcct,amount) is transaction
{ update OVERDRAFT_ALLOWED change CURRENT <-
if ACCT_NO=bankAcct then CURRENT + amount else CURRENT;
if [] where CURRENT > LIMIT in OVERDRAFT_ALLOWED then abort(Overdraw_b)
} compensated by transaction
{ update OVERDRAFT_ALLOWED change CURRENT <-
if ACCT_NO=bankAcct then CURRENT - amount else CURRENT
}
Note that compensated by can be interpreted as alt where the
signatures of the two blocks differ (as in Pay_cc), but
compensated by can only appear once for each alt-block, and is
not interpreted as alt if it has the same signature (as in Debit_b
and Overdraw_b). Well, maybe the first is a bad idea.
7. Let's try Aldat code using partial abort to process _all_ items in
CREDIT_CARD at once.
Before (note: different example)
CREDIT_CARD ACCOUNTS OVERDRAFT_ALLOWED
(ACCT_NO AMOUNT) (ACCT_NO BALANCE) (ACCT_NO LIMIT CURRENT)
1 $12 1 $10 3 $5 $0
3 $ 2 2 $10 4 $2 $0
4 $ 4 3 $ 1
4 $ 1
After
CREDIT_CARD ACCOUNTS OVERDRAFT_ALLOWED
(ACCT_NO AMOUNT) (ACCT_NO BALANCE) (ACCT_NO LIMIT CURRENT)
1 $12 1 $10 3 $5 $0
3 $ 0 2 $10 4 $2 $0
4 $ 4 3 $ 0
4 $ 1
update ACCOUNTS change BALANCE <- BALANCE - AMOUNT using CREDIT_CARD;
ACCOUNTS
(ACCT_NO BALANCE)
1 $-2
2 $10
3 $-1
4 $-3
update OVERDRAFT_ALLOWED change CURRENT <- CURRENT - BALANCE
using where BALANCE < 0 in ACCOUNTS;
OVERDRAFT_ALLOWED
(ACCT_NO LIMIT CURRENT)
3 $5 $1
4 $2 $3
update ACCOUNTS change BALANCE <- 0
using where CURRENT <= LIMIT in OVERDRAFT_ALLOWED;
ACCOUNTS
(ACCT_NO BALANCE)
1 $-2
2 $10
3 $ 0
4 $-3
abort(where CURRENT > LIMIT in OVERDRAFT_ALLOWED);
OVERDRAFT_ALLOWED
(ACCT_NO LIMIT CURRENT)
3 $5 $1
4 $2 $0
update CREDIT_CARD change AMOUNT <-0 using where BALANCE>=0 in ACCOUNTS;
CREDIT_CARD
(ACCT_NO AMOUNT)
1 $12
3 $ 0
4 $ 4
abort(where BALANCE < 0 in ACCOUNTS);
ACCOUNTS
(ACCT_NO BALANCE)
1 $10
2 $10
3 $ 0
4 $ 1
8. Evaluation and proposal.
Since abort() is being used in the sense of undo() and since we've
avoided any explicit commit() operator, let's replace abort() by
undo() (and aborted() by undone() ) and have no explicit abort()
operator. I.e., undo() undoes only what it says it will (partial undo),
and aborting transactions, like committing them, is left entirely to the
system and is not an option for the programmer. (We may need an aborted()
predicate to test this, but we'll see.)
Let's repeat the above seven notes under this proposal.
[BernNewc:TP] P. A. Bernstein and E. Newcomer, "Principles of Transaction
Processing", San Francisco, Morgan Kaufmann Publishers, Inc., 1997