# Source code for the P# toolchain

We provide the source code for the P# runtime (which includes the systematic testing schedulers) and the P# static
analyser. We also provide build instructions.

Note: The directories with the experiments contain prebuilt versions of the toolchain, so building from scratch is
completely optional.

## Contents

* psharp-runtime
  This dir contains the source code for building the P# runtime.

* psharp-static-analyser
  This dir contains the source code for building the P# static analyser.

## Build instructions: P# runtime

1. cd to the directory "psharp-runtime"
2. Open the "PSharp.sln" solution in Visual Studio 2015 Preview.
3. Switch to "Release" in the configuration manager.
4. Select "Build Solution" to build the P# libraries.
5. The binaries are placed in "\pldi15_artifact\1-psharp\psharp-runtime\Binaries\Release"

## Using the P# libraries

Include the "Microsoft.PSharp.dll" in your project and include "using Microsoft.PSharp;" above your namespace.
Please see one of our benchmarks in the other artifact directories as an example of building an application using P#.

## Build instructions: P# static analyser

1. cd to the directory "psharp-static-analyser"
2. Open the "PSharpStaticAnalyser.sln" solution in Visual Studio 2015 Preview.
3. Switch to "Release" in the configuration manager.
4. Select "Build Solution" to build the tool.
5. The binaries are placed in "\pldi15_artifact\1-psharp\psharp-static-analyser\Binaries\Release"

## Running the P# static analyser

Please see "\pldi15_artifact\3-static-analysis\README.md" for instructions.

## Where to find the implementation of core features discussed in the paper

1. The P# runtime (see Section 6.1 of the paper) is implemented in the "PSharp.sln" solution (in the "psharp-runtime" directory).

The core runtime functionality is implemented in the "Runtime.cs" file.
The core state-machine abstractions are implemented in the "Machine.cs" and "State.cs" files.
The systematic testing infrastructure (see Section 6.2 of the paper) is implemented in files inside the "Scheduling" directory.
The P# DFS scheduler is implemented in the "DFSSchedulingStrategy.cs" file.
The P# random scheduler is implemented in the "RandomSchedulingStrategy.cs" file.

2. The P# static analyser (see Section 5 of the paper) is implemented in the "PSharpStaticAnalyser.sln" solution (in the
  "psharp-static-analyser" directory).

The P# static analyser depends on and uses the Microsoft Roslyn code analysis APIs. The Passes directory includes the implementation
of the two main analysis passes that the static analyser performs:

* gives up ownership analysis, in the "MethodSummaryAnalysis.cs" file (see Section 5.2 of the paper).
* respects ownership analysis, in the "RespectsOwnershipAnalysis.cs" file (see Section 5.3 of the paper).

The Analyses directory includes (in the "DataFlowAnalysis.cs" file) the implementation of the data flow analysis that the
static analyser is built upon.

The xSA analysis (see Section 5.4 of the paper) is implemented in the "StateTransitionAnalysis.cs" file. This computes information
regarding the state transition graph of the program, which is then queried by other analysis passes to surpress false positives.
