Custom command semantics

[MattWindsor91]

PRQ #99 adds a new mid-level semantics for commands. This issue proposes opening up this mid-level semantics as a mini-language for adding custom commands.

Why? Because this will allow us to express symbolic commands easier, mainly. It also boosts our expressiveness story by allowing the user to 'choose' their atomic command set (while, at the Views level, the atomic commands are always fixed).

One possible syntax, shown in #104, is

atomic name(params) { microcode }

where

<params>         ::= <param> <params-rest>
<params-rest>    ::= <empty> | , <params>
<param>          ::= <class> <type> <lvalue-spec>
<class>          ::= shared | thread
<type>           ::= <prim-type> <array-spec>
<prim-type>      ::= int | bool
<array-spec>     ::= <empty> | [ <number> ] <array-spec>
<lvalue-spec>    ::= <identifier> | & <identifier>

<microcode>      ::= <microcode-step> <microcode-rest>
<microcode-rest> ::= <empty> | , <microcode>
<microcode-step> ::= <assign> | <forget> | <assume> | <conditional>
<assign>         ::= <lvalue> <- <expr>
<forget>         ::= forget <lvalue>
<assume>         ::= assume <expr>
<conditional>    ::= if (<expr>) { <microcode> } else { <microcode> }

where lvalue and expr are exercises left to the reader.

The idea is that if a parameter has a & before its name, it's restricted to being an lvalue, and appears in the write-to of the custom command. Each possible path through the command must assign or forget the parameter. The delimiter between microcode commands is , because it isn't sequential composition.

These atomic commands would only be allowed in angle brackets, to distinguish them from function calls (which might end up in Starling in the distant future).

Thus, CAS would become

atomic BCAS(shared bool &dest, thread bool &test, bool set)
{
    if (dest == test) {
        dest <- set, test <- test
    } else {
        dest <- dest, test <- dest
    }
}

// <BCAS(dest, test, set)>

and heap assignments from the LC list would become

atomic Unlock(shared int &heap, thread int prev)
{
    forget heap, %{unlock(#1)}(prev)
}

// <Unlock(heap, prev)>

The syntax can be tweaked around a lot though.

[septract]

This would be very useful in the MCS queue (see #133) where we need a compareAndSet operation over Starling variables. I want to write something like the following:

method unlock (Node qnode) { 
  ...
  < if (qnode == tail) { 
        tail = null;
        test = true; 
     } else { 
        test = false
     }  > ;  
  ...
} 

The only way to do this at the moment is (I think) to piggyback on GRASShopper's if statement, which is dumb:

method unlock (Node qnode) { 
  ...
  < test = ( tail == qnode ); 
    tail = %{ if ( [|test|] ) { [|qnode|] } else { [|tail|] } }; > ;  
  ...
} 

I think @MattWindsor91 also ran into this when he was trying to encode the Treiber stack.

[MattWindsor91]

Theoretically, atomic branches should be possible: they're supported in Microcode.

In practice, I'm not sure if the framing system will handle them properly. I think it will?

[MattWindsor91]

If we can implement branches without the custom command syntax, that means that all we need to do for the custom command syntax itself is lambda abstraction.

At this stage I'd honestly propose getting rid of the < command >; syntax entirely in favour of <{ syntax; }>; (or, personally, I think <| command; |> would be nicer), to clean up the language and because otherwise it'll get confusing as to what is allowed where.

[septract]

Yeah, I think <| command; |> would be nicer given we use curly brackets for a bunch of other things.

[septract]

I don't understand your first point: does this mean that branches are supported internally but aren't exposed by syntax?