Typed MachineIds - Githubissues

A simple approach.

MachineId<ClusterRuntime> id = CreateMachine<ClusterRuntime>();

// No static checking. But the type of the machine is at least known to the coder and the IDE.
// A static check could be added by the PSharp compiler
// (perhaps there should be a "PSharp checker" so that I can compile using Visual Studio
//  but still get some of the benefits of the PSharp compiler).
Send(id, EPrimaryRepReq);

A more radical approach, similar to how Fabric actors work.

IClusterRuntime clusterRuntimeMachine = CreateMachine<IClusterRuntime>();

// clusterRuntimeMachine is a proxy object created at runtime.
// The interface is generated at runtime (or compile time) by
// the PSharp runtime (or PSharp compiler).
// It is generated such that it implements IClusterRuntime and sends the event passed, as expected.

clusterRuntimeMachine.Send(e, payload);
// There will be a method in IClusterRuntime for each event type that is accepted.

It is not clear how IClusterRuntime is made though. In actors, the user writes it and implements it, and this defines the interface and implementation of the actor. (Perhaps there could be an alternative way of writing machines that does something like this? I can't think how though. Perhaps only if there were no states. This would also be nice because the payload(s) could be typed as well, although each event type would need to have fixed payload types.) Clients call an async method on the proxy object which causes a message to be sent to wherever the actor may be, containing the name of the method that was called and the serialized parameters. The async call/Task at the client completes when the remote actor has returned from the method.

For P#, the user could create the interface and "link" it to the machine somehow, and it could be checked at runtime (or compile time) that the event types included in the interface are handled by at least one state of the machine. But this would be tedious for the user.

Alternatively, the interface could be generated by the PSharp compiler (or checker). This is still a bit annoying, as it is a manual step when using the Visual Studio compiler (but if you want any of the existing static checks, then this is already the case). But then you may as well use the "simple approach". Although with this more radical approach, you at least get autocomplete.

(If you did adopt the Fabric actors style (perhaps further in the future), I can imagine things might look like this:)


IClusterRuntime clusterRuntimeMachine = CreateMachine<IClusterRuntime>();

// Event "EPrimaryReplicationRequest" (which is generated based on the
// PrimaryReplicationRequestSync method defined in IClusterRuntime)
// is sent to the clusterRuntimeMachine. 
// The payloads are the method parameters.
// Since this is a "sync" call, we wait here for an EPrimaryReplicationRequestResult event.

EPrimaryReplicationRequestResult res = clusterRuntimeMachine.PrimaryReplicationRequestSync(reqId, replicaId);

// Since this an async call, event "EPrimaryReplicationRequest" is sent, but we do not wait
// for a response. 
clusterRuntimeMachine.PrimaryReplicationRequestAsync(reqId, replicaId);

p-org / PSharp

Typed MachineIds #19