Public views

[MattWindsor91]

As a testbed for ideas about Starling's modularity, and based on ideas from @septract, we're considering adding a module system to Starling. The first, and perhaps easiest, thing to add would be a way of marking views and constraints 'public'.

Public views and constraints represent the surface of knowledge transfer that can leave the system described in a Starling file.

For example, the ticket lock would now look like:

public view holdLock();
view holdTick(int t);

constraint emp -> ticket >= serving;
constraint holdTick(t) -> ticket > t;
constraint holdLock() -> ticket != serving;
constraint holdLock() * holdTick(t) -> serving != t;
constraint holdTick(ta) * holdTick(tb) -> ta != tb;

public constraint holdLock() * holdLock() -> false;

Public constraints cannot name shared variables or non-public views. (In future, we might want to make it so they can name a public subset of shared state, but this needs some thought). As such, emp cannot ever be a public constraint.

This stage is fairly trivial to implement:

• Add public keyword to views and constraints;
• Add restriction of public constraints to public views;
• Add restriction of public constraints to parameters.

[septract]

We should talk about the theory behind this (also with @mjp41). Intuitively, it seems obvious that under this scheme we can verify modules and clients separately, but it's not captured in our current formalisation.

[MattWindsor91]

First thing is getting the specific soundness question down.

Are we trying to say that, in this case, given a proof C that borrows public views from a proof S, and that Starling |- S, then Starling |- C => Starling |- C * S for a certain combination operator * (which would basically be textual composition)?

[MattWindsor91]

The first result we could do with is that adding the defining views of S to C cannot invalidate the proof judgements of C, and vice versa. This would mean that |_ P _| for all P in C is unchanged by adding S and so on, so the views on both sides would need to be totally disjoint modulo public views.

What we need to do is work out exactly what C can do wrt naming public views in constraints. I think what we need to do is ensure that any constraint in C with a public view from S must be conjoined with a new view from C. This would in theory forbid the new constraint from being included in any reifications in C.

The other thing is that we need to be able to treat commands from C as hidden from views in S and vice versa. Command effects are always assignments, and local assignments are implicitly hidden from views anyway, so this becomes an appeal to the fact that the variable names are disjoint.

So, this is effectively proving that {| P |} x = ? {| P |} is true if forall x1, x2 : type x; |_ P() _|(x := x1) = |_ P _|(x := x2), and then presumably distribution laws for all of the other microcode command forms, I think. This should be fairly easy.

[MattWindsor91]

Though I presume that last idea needs rewriting in terms of the Starling proof rule.

[MattWindsor91]

@septract another thing I was wondering is, from an engineering point of view, how a client should use this. Would a client always be proven against a specific lock implementation (and thus just take its public views directly from the lock cvf), or would you have some sort of separated approach where the 'specification' of a lock in terms of public views would be written somewhere (in the client or in a third file) and Starling would check that the concrete lock obeys that specification on inclusion?

[MattWindsor91]

If we get a general set of proof modularity rules, theoretically speaking they shouldn't need a physical file boundary either.

You could imagine being able to analyse and partition single Starling files with several disjoint variable access patterns (but perhaps common pure views) into disjoint proof sections with their own set of defining views, variables, and axioms. Cutting down on the defining views per axiom would probably make more pathological proofs a bit faster to crunch through.

I wouldn't want to implement that though!