Machines that don't derive from "Machine"

[paulthomson]

One day, it might be nice to be able to create a Machine without actually having to derive from Machine. Deriving is ugly and can be problematic if you already have a class hierarchy (and you don't want to add " : Machine" at the top). All the (internal) machine info could be stored somewhere else. E.g. The PSharp runtime could wrap the object in a machine info object or store a mapping from the object to the machine info. The API methods can just be invoked via the PSharp runtime. As of the latest .NET, these can be imported statically so you can just type "CreateMachine" instead of "PSharpRuntime.CreateMachine" (although I quite like the latter anyway).

[pdeligia]

Hmm, this is an interesting idea, but I am not sure how this could be really achieved in a clean and robust way. I personally do not find deriving from a Machine ugly (I guess its also one of the compromises of using P# as a library versus the surface syntax), but I totally agree that it might be problematic if you have a large class hierarchy! One possible way would be to have some attribute and then the compiler will use this attribute to enforce some stuff on the class, and do possibly rewriting. But this would require huge changes all over the project, a lot of engineering and refactoring (unless it would coexist with the current approach, but I want to avoid giving too many baked-in options for doing the same thing as it makes stuff more confusing and harder to maintain). I am also not sure if something like this would bring a clear benefit over the current design, as we can already kinda achieve this separation of "machine" from a "class" with the following approach:

A machine can be used as a wrapper around a C# object (that might be a subclass of a large hierarchy of classes). The wrapper machine will basically act as the receiver of events from the environment (whatever that is, maybe P# or maybe C#), enabling the P# functionality of implicit enqueue and explicit send, and then whenever it receives some event, it will handle it by calling into appropriate methods of the wrapped object (after all actions can be arbitrary methods!). This gives full flexibility to the user to either write the whole logic in P# or only write the high-level state transitions in P# and keep his logic in old-good C# classes (that do not need to derive from Machine, but are essentially a machine because the objects "reside" inside a machine!) and even use the PSharpRuntime APIs from inside there (as it does not have access to the machine-specific methods) :-) I am currently using this technique in another project and works really well and requires minimal rewriting of the old code!

PS: I also prefer "PSharpRuntime.CreateMachine" rather than "CreateMachine", I actually do not like much this new feature, I always use the full namespace name to make things more readable!

[mattmccutchen-microsoft]

Some remarks:

• I took the approach of "move all the code to another class and leave the machine as a wrapper" when I ran into the restriction on nested classes other than states. But some of the protected Machine members that I wanted to use from the other class are not exposed on PSharpRuntime even though AFAIK they're not specific to the machine: Assert and Nondet.
• Even if the machines are only wrappers, there might be some reasonable use cases for sharing boilerplate code between machines (I don't have a good one right now). But currently machine inheritance doesn't work at all because the compiler wants the super-machine and the sub-machine to each declare their own start state (even if the super-machine is never instantiated), but then the runtime thinks the sub-machine has two start states. Example program:

using Microsoft.PSharp;

namespace PSharpTest
{
    class SuperMachine : Machine
    {
        [Start]
        class SuperState : MachineState { }
    }

    class SubMachine : SuperMachine
    {
        [Start]
        class SubState : MachineState { }
    }

    class PSharpTest
    {
        static void Main(string[] args)
        {
            PSharpRuntime.CreateMachine(typeof(SubMachine));
        }
    }
}

[pdeligia]

What you say about Assert and Nondet to be exposed as PSharpRuntime APIs is a good idea. I am not 100% sure if I should allow Nondet (although from a quick thought I cant see why not), but Assert should be definitely allowed.

Regarding the start state in machine inheritance, that is a bug and should be fixed -- let me look into this soon, thanks for catching it.

[paulthomson]

A static version of nondet should perhaps at least require a machineId for future-proofing. This allows each machine to have its own source of notdeterminism, which could be useful.

[mattmccutchen-microsoft]

For Nondet, the runtime can always look up the current machine from Task.CurrentId, and I don't think we'd want to allow a different machine to be specified, hence I don't think we need a parameter.

[paulthomson]

Ah yes. You're right. Sounds good. For some reason, I was thinking that the current machineId was required as a parameter for other methods (like Send), but it is not.

[pdeligia]

Btw, Nondet in the original P (i.e. $) is only used by a machine, and more specifically a model machine, as Nondet in real code does not probably make sense (only inside environmental modelling). I don't think this is enforced by the P# compiler right now. If someone uses Nondet in an actual machine it just returns a random boolean value (as if you used the Random API).

I also wonder if it matters if Nondet is called from outside a P#-machine (e.g. from C# code that is not wrapped by a machine). For random testing it does not really matter actually, as it always returns a fair random choice, and thus if there is a bug it will be randomly found if you keep exploring long enough, but I am not sure for stuff like DFS testing*. Although the general assumption is that there should be no non-determinism in the code that P# does not know about, if there is such-nondeterminism P# might still find bugs (due to the randomness in the choices). It would just not be able to replay (which is not currently supported anyway).

*DFS exploration takes into account not only the machine scheduling decisions, but also the random choices when it performs exploration, so it can capture both kinds of P#-based nondeterminism.

[afd]

On 17/07/2015 06:20, mattmccutchen-microsoft wrote:

Some remarks:

• I took the approach of "move all the code to another class and leave the machine as a wrapper" when I ran into the restriction on nested classes other than states. But some of the protected Machine members that I wanted to use from the other class are not exposed on PSharpRuntime even though AFAIK they're not specific to the machine: Assert and Nondet.
• Even if the machines are only wrappers, there might be some reasonable use cases for sharing boilerplate code between machines (I don't have a good one right now). But currently machine inheritance doesn't work at all because the compiler wants the super-machine and the sub-machine to each declare their own start state (even if the super-machine is never instantiated),

I see there have been a lot of follow-up emails that I have not yet read. But this brings to mind the notion of an abstract machine, akin to an abstract class - one that need not declare a start state. Would that make sense?

Ally

• but then the runtime thinks the sub-machine has two start states. Example program:

using Microsoft.PSharp;

namespace PSharpTest { class SuperMachine :Machine { [Start] class SuperState :MachineState { } }

 class  SubMachine  :SuperMachine
 {
     [Start]
     class  SubState  :MachineState  { }
 }

 class  PSharpTest
 {
     static  void  Main(string[]  args)
     {
         PSharpRuntime.CreateMachine(typeof(SubMachine));
     }
 }

}

— Reply to this email directly or view it on GitHub https://github.com/p-org/PSharp/issues/6#issuecomment-122178268.

[pdeligia]

@afd I think its mostly a bug in the static checker that I have to fix, without that static check (which triggers an error where it should not) it should work fine regarding the inheritance.

@mattmccutchen-microsoft I just exposed assert and nondet as runtime APIs. I am not doing anything special for nondet currently, I have to see if something special is needed (if someone uses it outside a machine).