p-org / psharp Goto Github PK

We should introduce wild card events that match against any possible type. I have two proposals. The first one addresses an immediate need while the second is more general.

First proposal is to introduce a keyword defer_all_else. One can use it as follows:

state S {
   on e1 do a1;
   on e2 do a2;
   defer_all_else;
}

In this case, all events except e1 and e2 (including halt) are deferred by the state.

The second proposal is to introduce a special event type called all_else or perhaps just *. One can use it in any state action (on action or ignore action or defer). But it can only be used once per state (no point using it more than once). For example:

state S {
   on e1 do a1;
   on e2 do a2;
   ignore *;
}

In this state, all events, not of type e1 or e2, are ignored by the state. Then defer_all_else is simply defer *.

One can argue both ways if the position of the wild card matters. That is, is on e1 do a1; ignore *; different from ignore *; on e1 do a1? I personally prefer that the wildcard match only appears as the last action on the state.

The first proposal is relatively easy to implement. The second will take more work. What do you think?

@pdeligia @shazqadeer

This is a bug. Fix it.

The current code seems to apply ignored events to the raise event as well:

                // Checks if the raised event is ignored.
                if (this.IgnoredEvents.Contains(nextEventInfo.EventType))
                {
                    nextEventInfo = null;
                }

My understanding is that in P, ignore/defer does not apply to the raised event. @shazqadeer

I'm working on a project that depends on some external assemblies. When I compile it with PSharpCompiler, the assemblies are not copied into the output directory and the program fails to load them at runtime. It looks like the code to link external assemblies is unfinished:

https://github.com/p-org/PSharp/blob/master/Source/LanguageServices/Compilation/CompilationEngine.cs#L293

Workaround: Build once with Visual Studio, then compile and test with PSharpCompiler as desired. The external assemblies remain in the output directory, so the program works.

I got an exception from the visual studio PSharp extension. Things still seem to be working though.

Microsoft Visual Studio
---------------------------
An exception has been encountered. This may be caused by an extension.



You can get more information by examining the file 'C:\Users\t-patho\AppData\Roaming\Microsoft\VisualStudio\14.0\ActivityLog.xml'.
---------------------------
OK   
---------------------------



  <entry>
    <record>525</record>
    <time>2015/06/24 07:13:57.325</time>
    <type>Error</type>
    <source>Editor or Editor Extension</source>
    <description>System.ArgumentException: Unable to find classification type for String tokenType&#x000D;&#x000A;   at Microsoft.PSharp.VisualStudio.PSharpClassifier.GetClassificationType(TokenType tokenType)&#x000D;&#x000A;   at Microsoft.PSharp.VisualStudio.PSharpClassifier.&lt;GetTags&gt;d__7.MoveNext()&#x000D;&#x000A;   at Microsoft.VisualStudio.Text.Tagging.Implementation.TagAggregator`1.&lt;GetTagsForBuffer&gt;d__1.MoveNext()</description>
  </entry>
</activity>

I opened Test.sln and then opened BaseServer.psharp (and closed it and repeated twice) in the AbstractPong project.

The tester should print the number of times executions hit max-steps number of steps

I need to implement a C# interface that contains a method that is called by C# code.

The method returns a Task<Operation> and the task blocks until some operation is available.

I implement the interface in a class called OStream. My current approach for the method is:

public Task<Operation> Get()
{
  return Task.Factory.StartNew(() =>
  {
    // wait for an event that satisfies some predicate 
    var eReq =
                    (EReq)
                        this.eventWaiter.WaitForEvent(
                            e => e is EReq);
    // notify some machine that this is the last event in this stream
    var eDone = new EStreamDone();
    PSharpRuntime.SendEvent(this.myNode, eDone, eDone);

    return eReq.operation;
  }
}

What is an EventWaiter?

    public class EventWaiter
    {
        private object monitor = new object();
        private IList<Event> events = new List<Event>();

        public Event WaitForEvent(Func<Event, bool> pred)
        {
           ...
        }

        public void PutEvent(Event e)
        {
           ...
        }
    }

The OStream class also creates a machine that has a reference to the event waiter and when it receives events, it calls PutEvent (inter-Task communication! Naughty!).

This works fine for me, but involves locks and inter-Task communication via the shared events list.

I feel that the "Action" argument to receive is not required. A receive should simply return the received event and then the user is free to execute his action. Further, Receive should not change this.ReceivedEvent, and avoid the (unexpected) side-effect.

This can considerably cleanup the Receive API.

I am getting a rare exception in Runtime.Send at the line:

var machine = PSharpRuntime.MachineMap[mid.Value];

The exception is System.Collections.Generic.KeyNotFoundException.

I think the race is in the constructor of MachineId on the line that does MachineId.IdCounter++. If two machines are created concurrently from different threads, then there can be a race on this variable. Perhaps this can be replaced with Interlocked.Increment(ref IdCounter) - 1.

It is quite confusing to explain why this race leads to the above exception, but I think it makes sense and, at the least, I think there is a data race on MachineId.IdCounter (when creating machines from different threads).

Minor changes can break tools (e.g. the change in machine output name for scheduling traces, broke the PSharpReplayer, see 25a136a) but we do not currently have tests in place to easily detect these kind of bugs.

It would be nice if we can come up with some unit tests, or maybe external regression suite if that is easier, since the tools are actual executables, similar to the basic scripts in the Sample directory.

This would give us 2 level of testing: existing unit tests for the P# libraries (core, language services and testing services), and a regression suite for the P# tools.

Like the one in ReplicatingStorage.

If Receive (the method that allows a machine to block inside an action to receive an event) is not a hack (i.e. not a last resort that users should avoid), then perhaps it should be async. If you had 100s of machines using the blocking Receive method, then you could end up having 100s of blocked Tasks which would exhaust the thread pool. Tasks are not supposed to be used like this. It can cause serious performance issues.

Making an async version of Receive would solve this. You would also need to allow async action handlers, but these would only be needed when async Receive is used.

An alternative quick fix would be to allow Tasks for certain machines to get their own thread in the thread pool (mark them as LongRunning). This is still not a real fix as you can end up with more threads than the number of threads in the thread pool.

(Requested by Nar)
1.

Wildcard matching:
on * do action;
or:
on * except e1, e2 do action;

Transitions common to all states should be declared on one place. For example we add on Timeout goto Terminating on all states in one shot.

In place of:
Instrumented 154 scheduling points (on last iteration).
We should say:
Average scheduling points in terminating executions: blah

It is useful to know the "expected" length of execution of a program. What do you think?

The following leads to a P# parse error:

event e<T>(f: T) where T: class;

On one of my bug-finding runs (without /v, so the bug trace would normally go to a file), the last ~250 lines of the ~1000-line bug trace went to the console. Theory of how this happened: Scheduler.KillRemainingTasks didn't kill all tasks because of a data race on this.Tasks, and then Runtime.WaitMachines got an AggregateException as soon as the first task was killed (see Task.WaitAll documentation) and returned without waiting for the rest of the tasks, so output was redirected back to the console while tasks were still running.

I've only seen this once and it wasn't with the latest version of P#, but if you think the problem could still happen, you may want to fix it. (Looks like P# could use some systematic concurrency testing!)

Halted machines are not reclaimed. Adding issue so we keep track of this.

We should have a way of running Visual Studio's code coverage along with P# tests.

In TaskMachineScheduler, the MachineTasks field is accessed without a lock. I don't know if this matters though. If it doesn't matter, you could add a comment.

I just synced up and tried to clean and rebuild PSharp.sln. I got the following errors:

Severity Code Description Project File Line
Error Metadata file 'C:\Users\qadeer\Work\PSharp\Binaries\Debug\Microsoft.PSharp.SystematicTesting.dll' could not be found SystematicTesting.Tests.Unit C:\Users\qadeer\Work\PSharp\Test\SystematicTesting.Tests.Unit\CSC
Error Metadata file 'C:\Users\qadeer\Work\PSharp\Binaries\Debug\Microsoft.PSharp.SystematicTesting.dll' could not be found Tester C:\Users\qadeer\Work\PSharp\Tools\Tester\CSC

After private discussions with @paulthomson and @shazqadeer, the current plan is the following:

Separate the PSharpCompiler.exe tool into two tools: a compiler and a tester

The user will be able to compile as now; or compile only a P# project and link with dll's that can be compiled in another arbitrary way. This allows more flexibility for projects that do not want to go through the Roslyn compiler, and also allows us to keep using the rewriting + static checking. A third option would be to compile everything from the user's build system, but then the user should not use raise + pop.

The tester will take the DLLs-under-test as now and test them.

This is related to #23

This is similar to #13

We are sometimes getting a KeyNotFoundException when sending an event. It again seems to be the case that a machine is "missing" from PSharpRuntime.MachineMap.

I am not quite sure of the exact sequence of events that causes this, but it does at least look like there is a data race on PSharpRuntime.MachineMap. If two machines are being created concurrently, then PSharpRuntime.MachineMap is being added to by both threads concurrently. Of course, other threads are also potentially reading from this map (which can be mutated at any time) when doing sends and so these reads should also be protected. Perhaps a thread safe map would be better.

If performance becomes an issue later, we could consider alternative solutions.

The P# compiler doesn't know about MsBuild. Thus, it cannot do things like copy the App.config file to the binaries folder.

I am currently implementing liveness property checking (basic support is done, the advanced features are implemented/tested in a new branch), similar to how P does this. This feature can be enabled using the /liveness command line option.

I give below a few different cases of how it can be used, and try to quickly explain it for now.

Case 1) The assumption in this case is that you have written a terminating harness. You can specify a liveness monitor as follows:

class M : Monitor
{
        [Start]
        [OnEventGotoState(typeof(Waiting), typeof(CanGetUserInput)]
        [OnEventGotoState(typeof(Computing), typeof(CannotGetUserInput)]
        class CanGetUserInput : MachineState { }

        [Hot]
        [OnEventGotoState(typeof(Waiting), typeof(CanGetUserInput)]
        [OnEventGotoState(typeof(Computing), typeof(CannotGetUserInput)]
        class CannotGetUserInput : MachineState { }
}

Notice the Hot attribute (can only be attached on a Monitor state). This denotes a state that progress is being waited to be made. If the program terminates and the monitor is in a hot state, then there is a liveness bug. You should make sure to transition a monitor to a non-hot state if the liveness property is satisfied (e.g. a node that just came up, received the data from the master). This way you can specify liveness properties as safety properties. But again reminder that this requires a terminating harness.

Case 2) The harness does not need to be terminating (e.g. can have infinite execution). You can write the same monitor as above. The P# runtime will perform some internal program state-caching (do not confuse with a machine state) and use it (together with the program trace) to identify a lasso (i.e. loop back to a previous program state). Then it will compute if this loop is a fair execution. If its not fair then it does nothing. If it is a fair execution, then it will check if the monitor was in a hot state at some point in the lasso. If yes, then it reports a liveness bug and exits.

Case 3) Same as above, but now you can write the following monitor:

class M : Monitor
{
        [Start]
        [Cold]
        [OnEventGotoState(typeof(Waiting), typeof(CanGetUserInput)]
        [OnEventGotoState(typeof(Computing), typeof(CannotGetUserInput)]
        class CanGetUserInput : MachineState { }

        [Hot]
        [OnEventGotoState(typeof(Waiting), typeof(CanGetUserInput)]
        [OnEventGotoState(typeof(Computing), typeof(CannotGetUserInput)]
        class CannotGetUserInput : MachineState { }
}

Note the Cold attribute (can only be attached on a Monitor state). This denotes a state that progress has been made. Follow the same algorithm as above. If there is a visited hot state and no cold state in the monitor during the loop, then report a liveness bug. Else skip the iteration as you just found an infinite loop that does not lead anywhere.

@p-org/p-developers @p-org/psharp-developers
Dear P and P# developers and users,
We are designing a visualization tool for P# programs and would like your opinion on it. The feature is checked into "visualization" branch of P#. The program visualizer summaries information from multiple runs of a P# programs and displays it in graphical format (with state machines and transitions). The user can interact with the tool to create their own view of the program.

There is a usage manual here:
https://github.com/p-org/PSharp/blob/visualization/Docs/Visualizer/VisualizerUsage.pdf

What do you think? We'd love to hear from you.

Akash & Pantazis

From @akashlal - if the user doesn’t supply iteration bound, can we make it to mean that only time budget should be used?

Deleted. Wrong post :-)

After discussions with some folks from production, there is interest in using the P# systematic testing engine without having to go through the P# compiler. This makes sense as there might be projects that have very sophisticated build systems, and we do not want to get into the business of trying to handle these kind of stuff.

This is possible in principle as the whole P# infrastructure is designed as a library and exposed through various APIs (versus a monolithic design). The actual P# compiler/analyzer/tester hybrid tool that we use today is built like this. So we could potentially also build a systematic tester that skips the compiler.

There are a couple of issues though: (1) we lose static analysis support for sanity checking that the code is as it should (e.g. no public fields etc); (2) we lose the minimal rewriting support that must happen even if someone does not use the high-level P# language.

Regarding the 2nd, if I recall correctly this only affects this.Raise(...); and this.Pop(); statements. These are normally rewritten to:

{ this.Raise(...); return; }
{ this.Pop(); return; }

In the past I tried to use exceptions for control flow, but this is not good design and is not bulletproof (as the user can just catch it). I am now trying to think ways to get around this. Feel free to post any thoughts/suggestions on this.

We would like to have full VS support, which would dramatically increase productivity. This is a really complicated matter though, especially due to how the P# parsing currently is done in a three phase approach. There are some suggestions:

(1) Directly extend Roslyn AST
(2) Extend the P# parser to handle advanced C# expressions/statements
(3) Embed P# as a C# framework

I am more inclined to do (1) or (2) as (3) would be too verbose and maybe harder to control? Have to think more about this ...

During Bug-finding mode, we should assert that Raise is called only from a top-level routine. I believe this requirement is not checked right now. There must be a way of inspecting the call stack in .NET?

When debugging, the debugger normally breaks on an uncaught exception. But the PSharp runtime catches all exceptions, reports the stack trace and then exits. It would be nice if this did not happen when debugging.

It looks like there is a way to achieve this:
http://stackoverflow.com/questions/21824597/catch-exception-if-debugger-is-not-attached

You create your try-catch blocks like this:

[DebuggerStepThrough]
static public void DoSomeStep()
{
    try
    {                
        DoSomething();
    }
    catch( Exception exception )
    {
        Console.WriteLine( exception.Message );
        if( Debugger.IsAttached == true )
        {
            throw;
        }
    }
}

The DebuggerStepThrough attribute ends up causing the debugger to break at the line where the exception was thrown originally (and not at the "throw" in the above method). The downside is that you cannot step through this method (without removing the attribute). However, it looks like you have a few small methods where you catch exceptions, so this seems like it would be fine: Do, ExecuteCurrentStateOnEntry, ExecuteCurrentStateOnExit (for both Machine and Monitor). And I doubt users will be stepping through these methods anyway.

Some comments suggest this only works if "Enable Just My Code (Managed Only)" is ticked, but I guess it's better than nothing.

Alternative: Only catch specific exceptions (e.g. TaskCanceledException) and add an unhandled exception event handler (or something similar).

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).

When registering anonymous action handlers, an extra semicolon is needed in the end. This looks awkward from a C# perspective. We should make it optional.

on e do { blah; blah; };

The liveness temperature threshold checking is turned off silently right now, if the underlying bug-finding scheduling strategy produces unfair executions (e.g budgeted strategies). We should ideally give some warning regarding this, or notify the user.

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);

I just synced up and tried to build as follows:

msbuild PSharp.sln

I got a lot of errors most having to do with 'nameof' e.g.,

TaskParallelism\DynamicError\SimpleTaskFailTest.cs(41,22): error CS0103: The
name 'nameof' does not exist in the current context [C:\Users\qadeer\Work\PShar
p\Test\SystematicTesting.Tests.Unit\SystematicTesting.Tests.Unit.csproj]

We should remove the /t flag from the compiler. Regardless of testing or execution, we should produce an exe (or what the project targets). Running the tester on an exe should not be an issue.

Currently garbage collection of machines is left to the user. The user must explicitly halt machines for them to be GCed. But we know that: if for a machine M, no other machine holds a reference to M.Id and M is idle, then it is going to remain Idle forever and it can be GCed. This route is difficult to implement; almost impossible given that we don't track heap objects. And many other languages make it known explicitly that actors must be halted to be GCed. In Orleans and Fabric, actors that have been idle for long are pushed out to disk and woken up only when needed.

We'll have to consider this design to support long-running P# programs.

The following lead to a P# parse error:

defer e;
ignore e;

In code using the P# framework APIs, I wanted an event to trigger both an action and a state transition. I overlooked the three-argument form of OnEventGotoState and tried to specify both OnEventDoAction and OnEventGotoState, which resulted in the action not running. Instead, this should be a compile-time error. (Low priority because the correct way to do this is stated in the manual.)

The following snippet results in a runtime failure "cannot find bar":

on evt do bar;

when bar is declared as a public method. This is because the action handlers must be declared private. To avoid surprises, we should statically check that all action handlers are declared as expected.

When I compile my code with PSharpCompiler (either using bug-finding mode or running the resulting executable), exceptions thrown by my code do not include line numbers in the stack trace. Line numbers would be helpful for debugging. For comparison (not a serious proposal of a workaround), if I build with Visual Studio, I do get line numbers. This is probably a matter of enabling generation of pdb files.

On http://p-org.github.io/PSharp/ it says:

A good way to start is by reading the manual (which is quite outdated right now, a new version will get released soon, but in the meantime please feel free to contact the P# dev team with specific questions).

The link is broken, but there is a maual, updated within the last two months, at https://github.com/p-org/PSharp/blob/master/Docs/Manual/manual.pdf

There is a difference in logging when using Machine.Send and RunTime.SendEvent, even when the latter is used to execute on behalf of a machine. This makes it hard to know the origin when using SendEvent.

Might be nice to add support for:

class Foo : Machine { ... }

and

machine { ... }

The following complains:

on default goto WaitForReq with
 {
  send(this.Target, Timeout);
}

Error: Special events 'halt' and 'default' cannot be generic.

When following the "machine core in another class" pattern (#6), I apparently nested an Event class inside the machine core class and wrote OnEventDoAction(typeof(MyMachineCore.MyEvent), ...). This caused a NullReferenceException in the new code at

Minimized example:

using Microsoft.PSharp;
using System;

namespace PSharpTest
{
    class MyMachineCore
    {
        internal class MyEvent : Event { }
    }

    class MyMachine : Machine
    {
        [Start]
        [OnEventGotoState(typeof(MyMachineCore.MyEvent), typeof(MainState))]
        class MainState : MachineState { }
    }

    class PSharpTest
    {
        [Test]
        public static void EntryPoint()
        {
            PSharpRuntime.CreateMachine(typeof(MyMachine));
        }
        static void Main(string[] args)
        {
            EntryPoint();
            Console.ReadLine();
        }
    }
}

Meta point: the output is pretty unhelpful:

C:\src\PSharpTest>..\PSharp\Binaries\Debug\PSharpCompiler.exe /s:PSharpTest.sln
..\PSharp\Binaries\Debug\PSharpCompiler.exe /s:PSharpTest.sln
. Parsing
Error: internal failure: System.NullReferenceException.

I had already modified my copy of P# to print the message and stack trace for internal errors, and you might consider the same. This still wasn't enough to find the problem, and I ran the compiler under the Visual Studio debugger. I had to comment out the uncaught exception handler in order for Visual Studio to break on the exception; compare to #12. If you can reproduce this behavior, you might see if there's a way to disable the uncaught exception handler when running under a debugger or otherwise remove the need to comment it out. (Of course, this doesn't matter to P# end users per se, but benefits contributors and sophisticated users who want to diagnose internal errors themselves.)

Here is my proposal from the pdev maillist:

If we think about it, P# (and P) is basically an actor-based language that provides (1) the state-machine based paradigm that forces users to think in terms of states and transitions, (2) modelling of environment using the substitution mechanism and (3) static analysis and testing. These 3 are kinda orthogonal to each other (although we exploit all of them to gain scalability and precision, etc).

Regarding (1) though, not everything in C# is translated to a state machine (e.g. something that requires a single state). Most protocols do, but in the C# world its very typical for various objects to exist around which are only in a "single state” receiving/sending events (in our message passing world).

To give users more options and easier integration with existing code, we could potentially provide a new construct in P# besides machine and monitors: the actor (or maybe some other name?). The actor behaves exactly the same as a machine (and reuses the underlying functionality of a machine in the runtime), but with a single difference: it has no states and state transitions (and thus no “on event goto state” or “raise statements"). Instead it has one single state (that is not visible by the user) and all action handlers are installed at actor level.

An actor would basically be syntactic sugar for a state machine with a single invisible state. An actor can communicate with a machine, and vice versa. It will still be amenable (completely out of the box) to the same static analysis + systematic testing we have currently and all the guarantees we provide. Of course you would be able to mix actors + machines + monitors.

The actor could be declared like this:

namespace PingPong
{
    [OnEventDoAction(typeof(Ping), "SendPong”)]
    internal class Server : Actor
    {
        MachineId Client;

        override void Create() { ... }

        void SendPong()
        {
            this.Send(this.Client, new Pong());
        }
    }

It would probably need to expose a new method to override, which acts as the constructor of the actor (similar to how the entry of the initial state is effectively a constructor).

I noticed that an event I declared as deferred was not being processed at all. It looks like a simple mistake here:

(Requested by Nar): Have a way of quickly asserting that a test covers a particular state.

Perhaps we can add an attribute to the state "assert must-be-reached" and a default monitor in the runtime that checks coverage.