Copyright ©2008 T. H. Merrett
COMP 617 Information Systems Winter 2008 Week 6
Undo in Aldat
1. Changes in event handlers: .trigger -> symdiff[]
An invocation of the system computation, symdiff, is better than a hidden
name, .trigger, and it is clearer if the result is simply always the
symmetric difference between the pre- and post-update states of the
relation being updated. This is symmetric in both pre: and post: event
handlers.
CREDIT_CARD ACCOUNTS
(ACCT_NO AMOUNT) (ACCT_NO BALANCE)
1 $2 1 $10
3 $2 2 $10
3 $ 1
4 $ 1
update ACCOUNTS change BALANCE <- BALANCE - AMOUNT using CREDIT_CARD;
ACCOUNTS symdiff[] post symdiff[] pre
(ACCT_NO BALANCE) (ACCT_NO BALANCE) (ACCT_NO BALANCE)
1 $ 8 1 $ 8 1 $ 8
2 $10 1 $10 1 $10
3 $-1 3 $-1 3 $-1
4 $ 1 3 $ 1 3 $ 1
post ACCOUNTS sjoin symdiff[] pre
(ACCT_NO BALANCE) (ACCT_NO BALANCE)
1 $10 1 $ 8
2 $10 2 $10
3 $ 1 3 $-1
4 $ 1 4 $ 1
Because A sjoin B sjoin A = B and sjoin is commutative and associative,
symdiff always allows us to reconstruct the alternative state of the
updated relation. Note, though, that we must explicitly do the ijoin with
the relation.
Note that symdiff is available only within event handlers - and within the
undo and redo computations we'll discuss from note 2 on.
This works for additions, deletions and assignments as well.
Let's try two event handlers for the above update under this new approach.
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 (ACCOUNTS sjoin symdiff[]))
};
ACCOUNTS symdiff[]
(ACCT_NO BALANCE) (ACCT_NO BALANCE)
1 $ 8
2 $10
3 $ 1 3 $ 1
4 $ 1 3 $-1
comp pre:change:ACCOUNTS[BALANCE]() is
{ let BAL be BALANCE;
update ACCOUNTS change BALANCE <- BAL using
((where BALANCE = 1 in ACCOUNTS) ijoin << note new condition >>
[ACCT_NO,BAL] in (ACCOUNTS sjoin symdiff[]))
};
ACCOUNTS symdiff[]
(ACCT_NO BALANCE) (ACCT_NO BALANCE)
1 $10
2 $10
3 $-1 3 $ 1
4 $ 1 3 $-1
2. Undo and Redo
We make an undo operation as a deferred event handler. (Ignore TAPE and
tape in the following example for the present. Also skip over callingComp
and parent and ignore undid and redid .)
update ACCOUNTS change BALANCE <- BALANCE - AMOUNT using CREDIT_CARD;
ACCOUNTS symdiff() post tape
(ACCT_NO BALANCE) (TAPE ACCT_NO BALANCE) 0
1 $ 8 0 1 $ 8
2 $10 0 1 $10
3 $-1 0 3 $-1
4 $ 1 0 3 $ 1
undo:change:ACCOUNTS[BALANCE](in "", in where BALANCE < 0 in ACCOUNTS);
uses the computation body
comp undo:change:ACCOUNTS[BALANCE](callingComp, condition) is
{ let BAL be BALANCE;
update ACCOUNTS change BALANCE <- BAL using
(condition ijoin [ACCT_NO,BAL] in
(ACCOUNTS sjoin [ACCT_NO,BALANCE] where TAPE=tape in symdiff[]));
tape <- tape - 1;
undid <- true; redid <- false;
parent <- callingComp
};
ACCOUNTS symdiff() tape
(ACCT_NO BALANCE) (TAPE ACCT_NO BALANCE) 1
1 $ 8
2 $10
3 $ 1 0 3 $ 1
4 $ 1 0 3 $-1
This computation body for undo can be generated automatically by the
system, so the programmer does not need to write it. But the programmer
must invoke it explicitly. So the undo computation works in a manner
directly opposite to the way an event handler works.
Note that if condition is empty, this means the undo is unrestricted
and the implementation changes slightly.
comp undo:change:ACCOUNTS[BALANCE](callingComp, ) is
{ let BAL be BALANCE;
update ACCOUNTS change BALANCE <- BAL using
[ACCT_NO,BAL] in
(ACCOUNTS sjoin [ACCT_NO,BALANCE] where TAPE=tape in symdiff[]);
tape <- tape - 1;
undid <- true; redid <- false;
parent <- callingComp
};
Redo is similar, but has no condition. Continuing the example,
redo:change:ACCOUNTS[BALANCE](self);
uses system-generated computation body
comp redo:change:ACCOUNTS[BALANCE](callingComp) is
{ let BAL be BALANCE;
tape <- tape + 1;
update ACCOUNTS change BALANCE <- BAL using [ACCT_NO,BAL] in
(ACCOUNTS sjoin [ACCT_NO,BALANCE] where TAPE=tape in symdiff[]));
undid <- false; redid <- true;
parent <- callingComp
};
ACCOUNTS symdiff[] tape
(ACCT_NO BALANCE) (TAPE ACCT_NO BALANCE) 0
1 $ 8
2 $10
3 $ 1 0 3 $ 1
4 $ 1 0 3 $-1
A further undo
undo:change:ACCOUNTS[BALANCE](self);
now gives the same result as the first undo. Note no condition this time.
Note that undo() precludes any other undo() of the same update, and in
particular one cannot undo the same update on different conditions.
We have left a lot of initialization up in the air, and the state variables
(which we have not discussed yet) tape, undid, redid and parent. Here is a
parent computation which generates undo and redo and several other things
which we'll come to. This computation can also be system-generated.
comp woops(rel,att,undo,redo,undone,redone) is
{ state intg tape;
state boolean undid, redid; << may want >1 undid, redid ! >>
state relation parent;
comp undo:change:rel[att](callingComp,condition) is ..
<< NB rel, att must be passed by name. >>
comp redo:change:rel[att](callingComp) is ..
comp undo:add:rel(callingComp,condition) is .. << T B A >>
comp redo:add:rel(callingComp) is .. << T B A >>
comp undo:delete:rel(callingComp,condition) is .. << T B A >>
comp redo:delete:rel(callingComp) is .. << T B A >>
comp undo:assign:rel(callingComp,condition) is .. << T B A >>
comp redo:assign:rel(callingComp) is .. << T B A >>
comp undone:..(name,toggle,yesno) is ..
comp redone:..(name,toggle,yesno) is ..
tape <- [red max of TAPE] in symdiff[];
undid <- false;
redid <- false;
parent <- "";
}
3. Multiple updates: undoing and redoing histories.
Now we discuss the TAPE attribute and the tape state variable. In the
context of undo and redo, symdiff[] also returns the attribute TAPE.
This distinguishes among different updates that symdiff[] may refer to.
Each update to the relation creates a fresh symmetric difference, which
is stored associated with a differnet value of TAPE, starting at 0.
The state variable, tape, is used to select the appropriate update and
symmetric difference. It is intialized in woops which is created and
invoked at the time of the first undo invocation. Its initial value
is the number of updates so far.
This TAPE/tape data structure is treated almost as if it were a stack.
In the following, the values of tape shown are those before the update,
undo or redo starts. (Except these values are hypothetical until the first
invocation of undo .)
Starting afresh. First update.
CREDIT_CARD ACCOUNTS
(ACCT_NO AMOUNT) (ACCT_NO BALANCE)
1 $2 1 $10
3 $2 2 $10
3 $ 1
4 $ 1
update ACCOUNTS change BALANCE <- BALANCE - AMOUNT using CREDIT_CARD;
ACCOUNTS symdiff[] tape
(ACCT_NO BALANCE) (TAPE ACCT_NO BALANCE) 0
1 $ 8 0 1 $ 8
2 $10 0 1 $10
3 $-1 0 3 $-1
4 $ 1 0 3 $ 1
Second time (new CREDIT_CARD)
CREDIT_CARD ACCOUNTS
(ACCT_NO AMOUNT) (ACCT_NO BALANCE)
2 $2 1 $ 8
4 $2 2 $10
3 $-1
4 $ 1
update ACCOUNTS change BALANCE <- BALANCE - AMOUNT using CREDIT_CARD;
ACCOUNTS symdiff[] tape
(ACCT_NO BALANCE) (TAPE ACCT_NO BALANCE) 1
1 $ 8 0 1 $ 8
2 $ 8 0 1 $10
3 $-1 0 3 $-1
4 $-1 0 3 $ 1
1 2 $ 8
1 2 $10
1 4 $-1
1 4 $ 1
The first conditional undo restores part of the second update.
undo:change:ACCOUNTS[BALANCE](in "", in where BALANCE < 0 in ACCOUNTS);
ACCOUNTS symdiff[] tape
(ACCT_NO BALANCE) (TAPE ACCT_NO BALANCE) 0
1 $ 8 0 1 $ 8
2 $10 0 1 $10
3 $-1 0 3 $ 1
4 $ 1 0 3 $-1
1 4 $-1
1 4 $ 1
The second conditional undo restores part of the first update.
undo:change:ACCOUNTS[BALANCE](in "", in where BALANCE < 0 in ACCOUNTS);
ACCOUNTS symdiff[] tape
(ACCT_NO BALANCE) (TAPE ACCT_NO BALANCE) -1
1 $ 8 0 3 $ 1
2 $10 0 3 $-1
3 $-1 1 4 $ 1
4 $-1 1 4 $-1
Now a redo repeats (the result of) the first update.
redo:change:ACCOUNTS[BALANCE](in "");
ACCOUNTS symdiff[] tape
(ACCT_NO BALANCE) (TAPE ACCT_NO BALANCE) 0
1 $ 8 0 3 $ 1
2 $10 0 3 $-1
3 $ 1 1 4 $ 1
4 $-1 1 4 $-1
And a second redo repeats (the result of) the second update.
redo:change:ACCOUNTS[BALANCE](in "");
ACCOUNTS symdiff[] tape
(ACCT_NO BALANCE) (TAPE ACCT_NO BALANCE) 1
1 $ 8 0 3 $ 1
2 $10 0 3 $-1
3 $-1 1 4 $ 1
4 $-1 1 4 $-1
Note that this pattern, undo, undo, redo, redo, gives the same result as
no undos or redos, or as undo, redo, undo, undo, redo, redo, or as ..
Symdiff[] does not return TAPE in the context of an event handler.
4. Communicating via undone, redone.
If we need to know that an undo has happened, and why, this can be
communicated by the boolean
if undone:change:OVERDRAFT_ALLOWED[CURRENT][in Pay_Bill, out toggle] ..
Here is an implementation, also supplied by woops . Undone allows us to
test for an undo either by the name of the computation that invoked the
undo , or by the name of the relation (rel) whose update was undone.
comp undone:change:OVERDRAFT_ALLOWED[CURRENT](name,toggle,yesno) is
{ yesno <- if name = parent then undid else
<>
if name = rel then undid else false;
toggle <- symdiff();
}
The implementation and use of redone are similar.
comp redone:change:OVERDRAFT_ALLOWED[CURRENT](name,toggle,yesno) is
{ yesno <- if name = parent then redid else
<>
if name = rel then undid else false;
toggle <- symdiff();
}
This explains the need for the state variables parent, undid and redid.
5. Application to the CREDIT_CARD payment example with OVERDRAFT_ALLOWED
(week3p1, note 7, corrected).
Before
CREDIT_CARD ACCOUNTS OVERDRAFT_ALLOWED
(ACCT_NO AMOUNT) (ACCT_NO BALANCE) (ACCT_NO LIMIT CURRENT)
1 $12 1 $10 3 $5 $0
2 $ 2 2 $10 4 $2 $0
3 $ 2 3 $ 1
4 $ 4 4 $ 1
After
CREDIT_CARD ACCOUNTS OVERDRAFT_ALLOWED
(ACCT_NO AMOUNT) (ACCT_NO BALANCE) (ACCT_NO LIMIT CURRENT)
1 $12 1 $10 3 $5 $1
2 $ 0 2 $ 8 4 $2 $0
3 $ 0 3 $ 0
4 $ 4 4 $ 1
comp Pay_Bill(CREDIT_CARD, ACCOUNTS, OVERDRAFT_ALLOWED) is transaction
{ update ACCOUNTS change BALANCE <- BALANCE - AMOUNT using CREDIT_CARD;
ACCOUNTS
(ACCT_NO BALANCE)
1 $-2
2 $ 8
3 $-1
4 $-3
We'll see at the end why we need the next 12 lines. Note (out ..)!
comp post:change:ACCOUNTS[BALANCE](out toggle) is {toggle <- symdiff[]};
ACCTsymdiff1 <- toggle;
ACCTsymdiff1
(ACCT_NO BALANCE)
1 $10
1 $-2
2 $10
2 $ 8
3 $ 1
3 $-1
4 $ 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 $ 8
3 $ 0
4 $-3
undo:change:OVERDRAFT_ALLOWED[CURRENT]
(in self, in where CURRENT > LIMIT in OVERDRAFT_ALLOWED);
OVERDRAFT_ALLOWED symdiff[]
(ACCT_NO LIMIT CURRENT) (ACCT_NO LIMIT CURRENT)
3 $5 $1 4 $2 $3
4 $2 $0 4 $2 $0
update CREDIT_CARD change AMOUNT <-0 using where BALANCE>=0 in ACCOUNTS;
CREDIT_CARD
(ACCT_NO AMOUNT)
1 $12
2 $ 0
3 $ 0
4 $ 4
The next undo won't work. (Why?)
undo:change:ACCOUNTS[BALANCE]
(in self, in where BALANCE < 0 in ACCOUNTS);
ACCOUNTS
(ACCT_NO BALANCE)
1 $10
2 $ 8
3 $ 0
4 $ 1
Instead, use ACCTsymdiff1, above.
FIX <- ACCTsymdiff1 sjoin where BALANCE < 0 in ACCOUNTS;
FIX
(ACCT_NO BALANCE)
1 $10
4 $ 1
let BAL be BALANCE;
update ACCOUNTS change BALANCE <- BAL using [ACCT_NO,BAL] in FIX;
ACCOUNTS
(ACCT_NO BALANCE)
1 $10
2 $ 8
3 $ 0
4 $ 1
} << Pay_Bill transaction >>
Note that undone:..[in Pay_Bill, out toggle] can tell us only about the
partial rollback of OVERDRAFT_ALLOWED.
But we can test for bounced payments with
where AMOUNT > 0 in CREDIT_CARD
6. Using nested transactions.
We can rework this closer to p.320 of [BernNewc:TP] (week3p1 note 4), where
nested transactions controlled updates at different hosts.
Pay_Bill
{ Pay_cc
Debit-b
if undone(Debit_b) then
{ Unpay_cc
Zero-b
Overdraw_b
if undone(Overdraw_b) then
{ Unpay_cc
Zero_o
}
}
}
Before
CREDIT_CARD ACCOUNTS OVERDRAFT_ALLOWED
(ACCT_NO AMOUNT) (ACCT_NO BALANCE) (ACCT_NO LIMIT CURRENT)
1 $12 1 $10 3 $5 $0
2 $ 2 2 $10 4 $2 $0
3 $ 2 3 $ 1
4 $ 4 4 $ 1
After
CREDIT_CARD ACCOUNTS OVERDRAFT_ALLOWED
(ACCT_NO AMOUNT) (ACCT_NO BALANCE) (ACCT_NO LIMIT CURRENT)
1 $ 2 1 $ 0 3 $5 $1
2 $ 0 2 $ 8 4 $2 $2
3 $ 0 3 $ 0
4 $ 1 4 $ 0
(This will be (maybe) better than before: we'll pay as much as possible of
every credit card.)
We assume there is an event handler post each update, returning symdiff[]
as toggle - which we may not always use.
comp Pay_Bill() is transaction
{ Pay_cc(out CCsymdiff1);
CREDIT_CARD CCsymdiff1
(ACCT_NO AMOUNT) (ACCT_NO AMOUNT)
1 $ 0 1 $12
2 $ 0 1 $ 0
3 $ 0 2 $ 2
4 $ 0 2 $ 0
3 $ 2
3 $ 0
4 $ 4
4 $ 0
Debit_b(in CCsymdiff1);
ACCOUNTS
(ACCT_NO BALANCE)
1 $-2
2 $ 8
3 $-1
4 $-3
ACCOUNTS
(ACCT_NO BALANCE)
1 $10
2 $ 8
3 $ 1
4 $ 1
if undone:change:ACCOUNTS[BALANCE][in Debit_b, out ACCTsymdiff1] then
ACCTsymdiff1
(ACCT_NO BALANCE)
1 $-2
1 $10
3 $-1
3 $ 1
4 $-3
4 $ 1
{ Unpay_cc(in where BALANCE < 0 in ACCTsymdiff1, out CCsymdiff2);
CREDIT_CARD CCsymdiff2
(ACCT_NO AMOUNT) (ACCT_NO AMOUNT)
1 $ 2 1 $ 0
2 $ 0 1 $ 2
3 $ 1 3 $ 0
4 $ 3 3 $ 1
4 $ 0
4 $ 3
Zero-b(in ACCTsymdiff1, out ACCTsymdiff2)
ACCOUNTS ACCTsymdiff2
(ACCT_NO BALANCE) (ACCT_NO BALANCE)
1 $ 0 1 $-2
2 $ 8 1 $ 0
3 $ 0 3 $-1
4 $ 0 3 $ 0
4 $-3
4 $ 0
Overdraw_b(in where AMOUNT > 0 in CCsymdiff2);
OVERDRAFT_ALLOWED
(ACCT_NO LIMIT CURRENT)
3 $ 5 $ 1
4 $ 2 $ 3
if undone:change:OVERDRAFT_ALLOWED[CURRENT]
[in Overdraw_b, out ODAsymdiff] then
ODAsymdiff
(ACCT_NO LIMIT CURRENT)
4 $ 2 $ 0
4 $ 2 $ 3
{ let BALANCE be if CURRENT <= LIMIT then CURRENT else LIMIT;
Unpay_cc(in [ACCT_NO, BALANCE] in OVERDRAFT_ALLOWED,
out ACCTSymdiff)
CREDIT_CARD
(ACCT_NO AMOUNT)
1 $ 2
2 $ 0
3 $ 0
4 $ 1
Zero_o();
OVERDRAFT_ALLOWED
(ACCT_NO LIMIT CURRENT)
3 $ 5 $ 1
4 $ 2 $ 2
}
}
}
comp Pay_cc(CCsymdiff) is transaction
{ update CREDIT_CARD change AMOUNT <- 0;
CCsymdiff <- toggle
}
comp Debit_b(CCsymdiff) is transaction
{ update ACCOUNTS change Balance <- BALANCE - AMOUNT using
where AMT > 0 in CCsymdiff;
undo:change:ACCOUNTS[BALANCE]
(in self, in where BALANCE < 0 in ACCOUNTS);
}
comp Unpay_cc(X,CCsymdiff2) is transaction
{ update CREDIT_CARD change AMOUNT <- AMOUNT - BALANCE using X;
CCsymdiff2 <- toggle
}
comp Zero_b(Y, ACCTsymdiff2) is transaction
{ update ACCOUNTS change BALANCE <- 0
using where BALANCE < 0 in Y;
ACCTsymdiff2 <- toggle
}
comp Overdraw_b(Y) is transaction
{ update OVERDRAFT_ALLOWED change CURR <- CURR + AMT using Y
}
comp Zero_o() is transaction
{ update OVERDRAFT_ALLOWED change CURRENT <- LIMIT using
where CURRENT > LIMIT in OVERDRAFT_ALLOWED;
}
The system may abort transactions or subtransactions due to crash or
conflict. We can suppose that such an abort in any subtransaction aborts
the entire parent transaction. Alternatively, we can suppose that
subtransactions support a checkpoint capability whereby the whole
transaction may be run again after a crash but all committed subtransactions
will be ignored on the rerun. In this latter case, consistency cannot be
guaranteed. (The first case violates the convention that nested transactions
do not abort the parent.)
The above transactions can readily be prefixed with aldatp protocol paths
so as to run on remote hosts.
[BernNewc:TP] P. A. Bernstein and E. Newcomer, "Principles of Transaction
Processing", San Francisco, Morgan Kaufmann Publishers, Inc., 1997