Add lists

[starsandspirals]

This PR adds lists as a new data type to Pat, and includes some small example programs as well as an extension of one of the Savina benchmarks.

We managed to fix a couple of the problems I was having, but there are still one and a half problems remaining:

• The "Pattern variable p0 was solved as pattern 0" issue (which may or may not be a real issue), currently happening in test/pat-tests/list-broken.pat
• The main issue where a list is being compared to a non-list for some reason, currently happening in test/examples/savina/kfork.pat

[starsandspirals]

Both problems listed above are resolved now. I've reorganised the Savina examples so that the original versions are in the main Savina folder, and the extended versions that use lists are in a subfolder (called, unsurprisingly, "lists"). The state of these so far is as follows:

• kfork.pat - implemented and typechecks
• cig_smok.pat - implemented but not working due to linearity difficulties
• big.pat - implemented but not working due to Pattern variables can sometimes occur after resolution #22
• banking.pat - WIP
• barber.pat - WIP (this one doesn't have a non-list implementation)

[starsandspirals]

Apologies it's taken so long as I've been working on recursive types in parallel, but this is basically ready for review and I've merged with the latest changes from main. However, since commit 56d2076 I'm having some trouble with quasilinearity in a couple of the examples that previously typechecked (which does also affect the recursive types work).

See lists/big.pat for the simplest example, though this also crops up in lists/barber.pat. The problem arises in the sink and sink_loop functions:

def sink(self: SinkMb?): Unit {
  guard self: Actors . (Done*) {
    receive Actors(exitMbs) from self ->
      sink_loop(self, exitMbs)
  }
}

def sink_loop(self: SinkMb?, exitMbs : [ExitMb!]): Unit {
  guard self: Done* {
    free ->
      notifyExits(exitMbs)
    receive Done() from self ->
        sink_loop(self, exitMbs)
  }
}

Because exitMbs is being received in an Actor message in sink, it is being deemed Usable, and so we aren't allowed to return it in the recursive call of sink_loop. However, in the non-list version of big.pat, the equivalent code returing three mailboxes typechecks:

def sink(self: SinkMb?): Unit {
  guard self: Actors . Done* {
    receive Actors(exitMb1, exitMb2, exitMb3) from self ->
      sink_loop(self, exitMb1, exitMb2, exitMb3)
  }
}

def sink_loop(self: SinkMb?, exitMb1: ExitMb!, exitMb2: ExitMb!, exitMb3: ExitMb!): Unit {
  guard self: Done* {
    free ->
        exitMb1 ! Exit();
        exitMb2 ! Exit();
        exitMb3 ! Exit()
    receive Done() from self ->
        sink_loop(self, exitMb1, exitMb2, exitMb3)
  }
}

so I think there must be something wrong with how quasilinearity is assigned to list (and other recursive) types. Unfortunately, I haven't been able to find it yet!

[SimonJF]

Hi @starsandspirals, after thinking about it and trying things out, the issue comes because it's only really sound to have returnable elements of a list, because otherwise we can introduce unsafe aliasing. Your examples require lists to contain elements with usable types. Consider the following example:

interface Test { M(Test!1) }

def drain(x: Test?): Unit {
    guard x : M* {
        free -> ()
        receive M(y) from z -> drain(z)
    }
}

def go(): Unit {
    let x = new[Test] in
    let xs = (x cons (nil: [Test![U]])) in
    caseL xs : [Test!] of {
          nil -> ()
        | (a cons as) -> x ! M(a)
    };
    drain(x)
}
go()

Here what we're doing is packaging x into a list, then deconstructing the list in the cons branch. However we now have both x and a in scope with different static names even though they refer to the same underlying runtime name. A litmus test for breaking soundness is sending a name to itself, as we've done here.

I fixed a small issue with disabling quasilinearity checking so please pull and recompile. Then running ./mbcheck with, and without -q will give two results: it's accepted without QL checking and (rightly) rejected with QL checking.

OK, so where does that leave us? In essence what you're trying to do is totally safe because you're not using any unsafe aliasing. In fact I think this is probably solvable in the same way that we solve the same aliasing problem for inter-process communication... So if we restrict the 'cons' branch to contain only free variables of unrestricted type (or mailbox types with a different interface) we should be able to rule this out while allowing your examples. Let me have a play and get back to you.

[starsandspirals]

Hi @SimonJF - thanks very much for fixing the issue with big.pat and barber.pat, but unfortunately the change has broken another example that was working before (banking.pat). I've simplified the logic in that example a bit now to use a sum type instead of a list in one case where the list could only ever contain one mailbox, but this didn't fix the quasilinearity problem. However, when I run this example with the quasilinearity check disabled, I get a failed assertion in type_utils.ml ... so maybe there's something weirder going on with this one as well!

[SimonJF]

Hi @starsandspirals -- sorry, GH didn't notify me of your comment! I'll have a look now.

[starsandspirals]

All examples are indeed working now (thanks for sorting all the issues we were having!) so marking as ready for review.

[SimonJF]

Thanks Danielle @starsandspirals for this great body of work and very welcome contribution! Minor changes requested really:

• Is there any way we can make the list type List(a) rather than [a], and ideally have an infix :: operator for cons?
• In fixing the join/intersect cases for lists I've realised there are some missing for tuples / sums. Please can you add the missing cases where indicated?
• As we found out, as long as we are careful about deconstructing things, we can treat lists as returnable regardless of whether their contents are usable or returnable. The same logic applies to tuples and sums, so if you can please make the indicated changes?
• Can you please add the new lists examples and tests to the test suite JSON file?

Thanks again!

[SimonJF]

Again based on my argument in make_returnable these should all be returnable by default.

[starsandspirals]

Fixed these - is make_usable fine as is?

[SimonJF]

I don't suppose there's any way we can get an infix :: going?

[starsandspirals]

Done - assume okay to leave nil as "nil" rather than "[]" since this could be again confused with quasilinearity annotations?

[starsandspirals]

Hi @SimonJF - sorry for the delay but think I've handled all the requested changes. See a couple of minor questions from me above but otherwise hopefully good to go!