PSharp
PSharp copied to clipboard
p-org
A framework for rapid development of reliable asynchronous software.
I thought this method being rather empty was a bug. But apparently, this may not matter because the CycleDetector gets recreated every iteration. However, we could still consider NOT doing...
It should be possible to assert things inside the P# runtime or inside a SchedulingStrategy. If these fail, this is not a bug in the program under test, but a...
@pdeligia and I have been discussing the default event handler. Is it an essential feature? I am not sure how to soundly reason about this as a visible operation. If...
In a P# program, the expectation is that async methods are always awaited. The compiler gives a warning by default. We should change it to be a compilation error by...
It should return only when all machines have finished their current action (and are idle or stuck at dequeue)
1. Handle comments in BlockSyntaxVisitor. Currently, a { or } in a comment confuses things. 2. Comments in the P# section are not written to the rewritten *.psharp.cs file. 3....
Currently we error on assignment to fields of the machine, such as: a. const string foo = “bar”; // error at 'string') b. string foo = "bar”; // error at...
We should think about the topic of doing testing of `P#` programs running with the production runtime. We cannot hope to be systematic or provide reproducible traces, but we can...
The race detector cannot find racing accesses to a collection (like List, Dictionary, etc.) because we do not instrument mscorlib. We should have means of adding this knowledge, e.g., List.Add...