[m-dev.] STM rewrite

[Chris King]

On Wed, Nov 9, 2011 at 2:37 AM, Peter Wang <novalazy at gmail.com> wrote:
> Would if-then-else behave differently at all to or_else?

if-then-else would actually be a superset of the behavior provided by
or_else.  Here's an example using the old STM implementation:

atomic [outer(!IO), inner(!STM)] (
    transfer(Acct1, Acct3, !STM)
or_else
    transfer(Acct2, Acct3, !STM)
)

This code should atomically transfer money from Acct1 to Acct3, or
failing that, transfer money from Acct2 to Acct3, or failing that,
block until there is enough money in either account.  The invariant
that Acct1 has insufficient funds holds true in the second branch.
(Note: I believe there is a bug in the old STM implementation which
makes this invariant not true.)

The equivalent using the new implementation would be:

atomic [outer(!IO), inner(!STM), retry_on_fail] (
    if transfer(Acct1, Acct3, !STM) then
        true
    else
        transfer(Acct2, Acct3, !STM)
)

Note that we can put something where "true" is!  So we could write:

atomic [outer(!IO), inner(!STM), retry_on_fail] (
    if transfer(Acct1, Acct3, !STM) then
        transfer(Acct2, Acct4, !STM)
    else
        transfer(Acct2, Acct3, !STM)
)

This means, block until either there's enough money in Acct1 to pay
Acct3 and enough money in Acct2 to pay Acct4, or if there's not enough
money in Acct1, pay Acct3 from Acct2 instead and forget about Acct4.
(Sorry if this is confusing!)  To accomplish the same in the old
syntax would require helper variables:

atomic [outer(!IO), inner(!STM)] (
    atomic [outer(!STM, inner(!STM2)] (
        transfer(Acct1, Acct3, !STM2),
        Success = yes
    or_else
        transfer(Acct2, Acct3, !STM2),
        Success = no
    ),
    (
        Success = yes,
        transfer(Acct2, Acct4, !STM)
    ;
        Success = no
    )
)

With the new syntax we can also do fun things with negation and scoping:

atomic [outer(!IO), inner(!STM), retry_on_fail] (
    not dequeue(Queue, _, !.STM, _),
    enqueue(Queue, Elt, !STM)
)

This will block until the given queue is empty (i.e. it cannot dequeue
anything), and then atomically insert Elt into the queue.  Another:

atomic [outer(!IO), inner(!STM), retry_on_fail] (
    transfer(Acct1, Acct3, !.STM, _),
    transfer(Acct2, Acct3, !STM)
)

This will transfer from Acct2 to Acct3 *only if* transferring from
Acct1 to Acct3 would succeed.  (At the moment, this only compiles
because the stm type is not mostly_unique.  If it were, we'd need to
use an awkward "if not" construct, because Mercury doesn't realize
that since the first line binds no output variables, it can backtrack
the mostly_unique !.STM.  Preposing the first line with "not not" or
"all []" doesn't work since Mercury eliminates double negation.)

> I second your suggestion to explicitly mark atomic blocks for
> retry-on-failure, simply because I would hate to write a semidet goal
> accidentally (although we do have determinism check scopes now).
> I suggest the flag `retry_on_fail' :-)

Sounds good!  I was also thinking "may_block" but "retry_on_fail" is
more descriptive.

- Chris
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at csse.unimelb.edu.au
Administrative Queries: owner-mercury-developers at csse.unimelb.edu.au
Subscriptions:          mercury-developers-request at csse.unimelb.edu.au
--------------------------------------------------------------------------