[proposal] MPCal archetype paremeters in Go

[fhackett]

This is an issue documenting my ideas regarding translating MPCal archetype parameters into Go.

The general principle I've been operating under is that a parameter would be an instance of an interface like this:

type Access int

const (
    R Access = 1 // 01b
    W Access = 2 // 10b
    // RW = R|W = 11b is implied
)

type ArchVariableT interface {
    // called at the beginning of any critical section that needs the variable
    // returns the value of the variable in all cases except
    // access == W, nil in that case
    Acquire(access : Access) T
    // writes the value to the variable and ends the critical section,
    // panics if !(access & W)
    Commit(value : T)
    // ends the critical section with the value of the variable unchanged
    Abort()
}

Obviously T is not a real type and Go's lack of generics will as usual cause pain for code generators... but hopefully this gets the point across.

Here is an example of an archetype and its compilation (sorry if I got a compilation detail meaningfully wrong):

archetype ArchFoo(ref a, ref b) {
    section1:
    a := 1;
    section2:
    b := a || a := b;
    section3:
    either { a := 2; await b = 2; } or { skip };
}

func ArchFoo(a, b : ArchVariableInt) {
    // section1
    a.Acquire(W)
    a.Commit(1)
    // section2
    aVal, bVal := a.Acquire(R|W), b.Acquire(R|W)
    bVal, aVal := aVal, bVal
    a.Commit(aVal)
    b.Commit(bVal)
    // section3
    for {
        // option1:
        a.Acquire(W)
        bVal = b.Acquire(R)
        aVal = 2
        if bVal != 2 {
            a.Abort()
            b.Abort()
            goto option2
        }
        a.Commit(aVal)
        b.Abort() // not really an abort, but it just has
            // to "end the critical section with no write" so it's ok
        break
        option2:
        break // skip
    }
}

[rmascarenhas]

Thanks for the writeup, @fhackett. As usual, I have a few comments/questions :-)

I guess I had a very different idea of how we would approach the compilation of archetypes to Go (or maybe they are similar and I'm failing to see). The approach of acquire/commit/release is very similar to what we currently have for PlusCal processes, and as such I'm failing to see the advantage of archetypes since we are still relying on the abstraction of a global shared address space (with the massive overhead that it entails in a distributed context). In addition, if the operations are essentially the same, why would we need a new API instead of using the existing global state management API?

As an aside, archetypes would really shine if we were able to provide a "channel" abstraction in the implementation while still allowing specs to use variables as is typically done in PlusCal (and that was sort of the motivation to begin with).

We had a discussion some weeks ago where we discussed a possible compilation strategy, so I'm going to document it here too (for the same archetype ArchFoo you defined above):

type Channel interface {
  Read() (error, interface{})
  Write(interface{}) error
}

type RPCChannel {
    // ...
}

func (c *RPCChannel) Read() (error, interface{}) {
    // ...
}

func (c *RPCChannel) Write(val interface{}) error {
    // ...
}

// For simplicity of exposition, no error checking.
func ArchFoo(Channel a, Channel b) {
    // section1
    a.Write(1)
    // section2
    aVal, bVal := a.Read().(int), b.Read().(int)
    bVal, aVal := aVal, bVal
    a.Write(aVal)
    b.Write(bVal)
    // section3
    for {
        // option1:
        bVal = b.Read().(int)
        aVal = 2
        if bVal != 2 {
            goto option2
        }
        a.Write(aVal)
        break
        option2:
        break // skip
    }
}

This does force the spec to be written in a "message-passing style" as opposed to treating everything as a single global address space (and this is precisely what I said in a Google Docs I shared some time ago detailing my experience converting PlusCal specs to MPCal: in the latter, it feels like you have to think of the resulting implementation more often).

Another thing we discussed (not sure if you were around) is that we should probably provide a "standard library" of mapping macros for common network semantics (UDP, TCP, etc) and corresponding runtime implementations of theChannel interface above.

Finally, I think we should still support (but discourage) the abstraction of a globally accessible variable with permissions/acquire/release API, but I think we can stick with the existing implementation and API in that case.

[fhackett]

@rmascarenhas thanks for your questions - I see I forgot to explain the relationship I see between our ideas.

Here is an adapter between your channel semantics and the API I described:

type ChannelVar Channel

func (self *ChannelVar) Acquire(access Access) T {
    if access & R != 0 {
        return self.Read()
    }
    return nil
}

func (self *ChannelVar) Commit(T value) {
    self.Write(value)
}

func (self *ChannelVar) Abort() { }

This will of course only be a correct implementation of my API if the MPCal algorithm uses the variable as if it were a channel, but that's the point. If we know that variable is a channel then the above implementation (give or take some details like whether it should latch the last value received) is perfectly adequate and most of the concurrency control semantics are redundant in this case.

If however you had a variable that did not match those semantics then you could instead provide another implementation with stronger guarantees (and worse performance), like something backed by our existing value store.

Hopefully this explains things better - let me know if I forgot something else / you find any flaws in my idea(s).

[rmascarenhas]

I see, that does make sense, @fhackett! Thanks for making it clear. I think the ArchVariableT interface you proposed can be implemented on top of the existing distributed state API (just being thin wrappers to the existing calls).

But other than that, I guess we are on the same page :+1:

[rmascarenhas]

The runtime part of this is mostly implemented, so I'm closing this issue.