• Messages sorted by: [ date ][ thread ][ subject ][ author ] [ Next ]
• [ Previous ] Next in thread: Mark S. Miller

MarkM wrote:
>
> Ping, there's a lot of meat here, and a reply will be meaty as well. Would
> you like to resend your message to the E list, so that I can reply there as
> well? Thanks.

Certainly.

The message is included below for all to peruse... (and tear apart).

Precontext: this is a response to MarkM's ERTP, a wonderfully minimal and simple spec that he showed me last night; specifically it's about the Cambio example he uses to illustrate ERTP.

Postcontext: there is a comment about naming the deposit method here, but the rest of the message is really about a more general issue of transaction management and atomicity. The deposit method provides a little extra atomicity good for some simple cases, but without a general way to do locking or reversible transactions you can't then compose new compound operations out of the elementary ones in ERTP that remain safely atomic.

e.g. My musings below attempt to make the two-party exchange transaction fairly safe, but what if you wanted to build some more complicated kind of transaction that involved two Cambios? It's not clear to me that you could continue ensuring risk-free transactions between the parties.

I'm not sure how to address this since E and locking don't seem to mix.

• ?!ng

"What would this country be without this great land of ours?"

• Ronald Reagan

  ---

On the way home, i realized that it might be best to make the method name "depositInto" rather than "depositAll" or "depositFrom". Motivations:

1. People are used to source first, destination second. In your Assay transfer method, you go along with this convention. It seems natural to use the same ordering for transferring an entire purse's contents also. So: sourcePurse depositInto(destPurse).
2. When you talk about capabilities the "feel" i get is that you are calling a method on the thing whose rights you want to invoke. I know that in this case, the two purses are in cahoots and are simply agreeing to do the transfer with each other, but it still feels right to be calling the method on the thing that has the rights i am invoking, i.e. the purse from which i am *withdrawing* the rights. It makes more sense to me to say to the sourcePurse, "please give your rights to this other purse here", rather than saying to the destPurse, "please steal some rights from this purse". (Or, in fewer words, Alice first.)

Here is my go at a rewrite-from-memory of the Cambio's currency-conversion method, picking names that seem natural to me:

to convertPurse(srcPurse) {

        define inAssay := srcPurse depositInto(inPurse)
        try {
            define outAssay := convertAssay(inAssay)
            define destPurse := outPurse.issuer makePurse
            outAssay transfer(outPurse, destPurse)
            destPurse
        } catch exception {
            inAssay transfer(inPurse, srcPurse)
            throw exception
        }

Notice that there is still a potentially important problem with this method: it is still possible for the refund to fail, since during the time between depositInto(inPurse) and transfer(inPurse, srcPurse) funds might be removed from the inPurse and there might no longer be sufficient funds available to be returned.

A second attempt:

to convertPurse(srcPurse) {

        define holdingPurse := inPurse.issuer makePurse
        define inAssay := srcPurse depositInto(holdingPurse)
        try {
            define outAssay := convertAssay(inAssay)
            define destPurse := outPurse.issuer makePurse
            outAssay transfer(outPurse, destPurse)
            holdingPurse depositInto(inPurse)
            destPurse
        } catch exception {
            holdingPurse depositInto(srcPurse)
            throw exception
        }

I think this one is "provably" safe, assuming that depositInto can be relied upon never to throw an exception so long as the argument is a purse from the correct issuer. Any other method call should be able to fail in this example without damaging the rules of the transaction.

The first thing that happens in the method is to dump the contents of the srcPurse into the holdingPurse. The holdingPurse matches the *inPurse* type, not the srcPurse type, so this depositInto can fail right away if the srcPurse is the wrong kind.

Only after that succeeds has the srcPurse become empty. Now the holdingPurse contains the received rights and we have verified that they are of the right kind.

After that, there are clearly exactly two possibilities: success or failure of the "try" clause.

The last thing that happens in *either* case is for the contents of the holdingPurse to be dumped somewhere. If it is dumped into the inPurse, then the outAssay transfer must have succeeded. If not, then it clearly must be deposited back into the srcPurse. We have already determined that the holdingPurse is compatible with the srcPurse, and the holdingPurse is compatible with the inPurse by construction, so neither of these deposits can fail.

Look right to you?

(It is clear to me now that a statement of exactly what exceptions may and may not be thrown by each method is an absolutely essential part of the ERTS specification. Actually, the more i think about it the more concerned i am about exceptions: they seem to be the main thing that could make smart contracts very tricky to verify.)

Hmm. A third possibility:

to convertPurse(srcPurse) {

        define holdingPurse := inPurse.issuer makePurse
        define inAssay := srcPurse depositInto(holdingPurse)
        try {
            define outAssay := convertAssay(inAssay)
            define destPurse := outPurse.issuer makePurse
            outAssay transfer(outPurse, destPurse)
            holdingPurse depositInto(inPurse)
            destPurse
        } catch exception {
            holdingPurse
        }

In this case, you lose the information about what happened when an exception is raised, but i *believe* that you are guaranteed to get your equivalent value back in the returned possibility no matter when any method decides to raise an exception: the catch clause can never fail.

And finally, a fourth possibility:

to convertPurse(srcPurse) {

        define holdingPurse := inPurse.issuer makePurse
        define destPurse := outPurse.issuer makePurse
        define inAssay := srcPurse depositInto(holdingPurse)
        try {
            define outAssay := convertAssay(inAssay)
            outAssay transfer(outPurse, destPurse)
            holdingPurse depositInto(inPurse)
            destPurse
        } catch exception {
            try {
                destPurse depositInto(outPurse)
            } catch exception {
            }
            holdingPurse
        }

This one attempts to protect both the user and the creator of the Cambio in case of failure. In the third example, the owner of the outPurse could lose money if somehow the last deposit fails; in this example there's an attempt to account for that. (But it might be pointless here anyway, since the attempt to restore the funds might also fail; at some point, you just have to rely on depositInto.)

• ?!ng

"Computers are the tools of the devil. It is as simple as that. There is no monotheism strong enough that it cannot be shaken by Unix or any Microsoft product. The devil is real. He lives inside C programs." -- philg@mit.edu

[ Next ]
• [ Previous ] Next in thread: Mark S. Miller