modal harmony

[nikomatsakis]

The "modal harmony" branch is my attempt to "revamp" dada by adding "modes" to variables. This is a tracking issue covering the plan and pending work and decisions.

The plan

• modal harmony tutorial #143 updates tutorial to describe the new model

If we make further changes (e.g., see the unresolved questions below), will add new PRs here.

Implementation steps

• Modal harmony #148:
  • Introduce modes on local variables, parameters, fields
  • Assigning to an lvalue with mode m applies the appropriate operation (e.g., assigning to a my variable is a give, etc)
  • Calling a function whose parameter has mode m also applies that effect to the
  • Check that variables have adequate permissions (e.g., assigning to a my requires unique ownership)
• Introduce shlease keyword and shleased mode (currently our leased in Modal harmony #148)
• Modify print to not print permissions and to shlease its arguments, just as user code would do

Unresolved questions

Names for the modes

Currently the modes are as follows.

	Unique	Shared
Owned	my	our
Leased	leased	shleased

There are also the following "verbs" to transform permissions:

• o.give produces another value with same permissions as o
• o.share moves "one slot" to the right, so given a my value it produces an our, given a leased value you get back a shleased
• o.lease moves "one slot" down, so given a my value you get a leased, given an our you get a shleased

I am pondering whether the following names would be better:

	Unique	Shared
Owned	owned	shared
Leased	leased	shleased

They are longer, which is a drag, but they are more consistent.

[nikomatsakis]

Other random names and thoughts I figured I might as well jot down. I've been pondering the names. shlease really feels like a non-starter the more I think about it. :)

Read and write. We could call the leased modes "read" and "write" (and the verbs to get them .read and .write). So then you would have a "write lease" or a "read lease" (but a "read" lease also lets you write atomic fields, which is weird).

	Unique	Shared
Owned	my	our
Leased	write	read

Interesting thing, given some my m, then m.share would be our and m.read would be read.

Leased and shared. We could call the leased modes "leased" and "shared", but in that case foo.share cannot yield our. That got me to thinking that maybe rather than "unique" and "shared" it should be like "whole" and "split" or something:

	Whole	Split
Owned	my	our
Leased	leased	shared

Then you would do:

my m = Object()
our o = m.split

or

shared o = m.share

You could apply split to a leased value to get a shared value, as usual too.

Can we get rid of shleases? Of course the big question is if we need the idea of a shlease. I considered a few alternatives. At some point I wanted to foo.lease.share be equivalent to foo.shlease, but the problem I realized was that foo.lease creates a leased l that is promised unique access to foo, and then a shared sublease of l, so you still cannot access foo without canceling the original lease l. I considered a rule ("house parties") that said "if there is a shared sublease of foo, then you can read directly from foo without canceling the intermediate lease", but I was nervous about it. It seems to go against Rust patterns used by the Mutex struct and other structs. I'm having a harder time coming up with an example of how it fails in the "atomic" world of dada, but it still seems off to me. I think the counter example is this (using (what I imagine) fully typed Dada (will look like) for clarity; I'll use the name shared to mean "shleased", and .share to mean "convert a unique value into a shared one):

class Counter(our n: Int)
class Atomic(my atomic c: Counter)

fn get_counter(leased l: Atomic) -> shared Counter {
    # We can access `l.c` without an atomic section, since 
    l.c.share
}

my a = Atomic(Counter(0))

# Lease a but then get back a sublease to `a.c` that is shared
shared c = get_counter(a.lease)

print(c.n).await # prints 0

# Shared lease of `a` and then atomically mutate the counter `n`
shared a1 = a.share
atomic {
    a1.c.n += 1
}

print(c.n).await # prints ? -- at this point, `c.n` should not have changed, but it did

There are some assumptions in this example, though. I'm assuming that sharing a would be allowed despite the lease l because of the sublease of l.c, but maybe that is the flawed assumption. The house party rule could only apply to the entire object, in which case a.share would invalidate c.

from. I've been pondering also what I want the fully typed, non-elided forms to look like. I am expecting something like this:

fn get_counter(leased l: Atomic) -> shared(l) Counter {
    # We can access `l.c` without an atomic section, since 
    l.c.share
}

where shared(l) means "shared from l (the leased variable). I was briefly just now pondering if shared Foo could (by itself) mean our Foo but shared from(l) Foo would mean "leased", and hence "from" would be the keyword to signal that, but I think it doesn't work.

Conclusion. Nothing really, just that I need to come up with a canonical set of examples I can use to illustrate the various options. I have a bunch of modes, combinations and examples floating in my head and it's hard to remember them all at once! Going to work a bit on that.

[nikomatsakis]

Diagram

     my  ───share────►  our
     │ │                │
lease│ └────┐           │ lease
     │      │shlease    │ shlease
     │      └────┐      │
     │           │      │
     ▼           └───┐  ▼
                     ▼
   leased───────────►shleased
            share
            shlease