The initializer for the "union" part of the PRT_TYPE and PRT_VALUE structs in the generated code need to be surrounded by another level of curly braces, for example, this:

  PRT_TYPE P_GEND_TYPE_0 = 
  {
    PRT_KIND_ANY,
    NULL
  };

needs to be this:

  PRT_TYPE P_GEND_TYPE_0 = 
  {
    PRT_KIND_ANY,
    { NULL }
  };

After my recent fixes to deal with static functions, I am now getting a link error when I compile the generated C code using the solution files in the respective folders.

Error 51 error LNK2019: unresolved external symbol _PrtEnqueueWithInorder referenced in function _s_PrtDistSendEx C:\Users\qadeer\Work\P\Src\PrtDist\Samples\TechFest2015-Demo\PrtDist.lib(PrtDist.obj) FailureDetector

This assertion fails in Zinger. Should it?

Eq.p:

type F;
type G = F;


main machine MyMachine
{
    start state Init
    {
        entry
        {
            var f : F;
            var g : G;

            assert f == g;
        }
    }

}

Take care of following Integration/Correct
10/01/2015 05:48 PM

This is a "nice to have feature", but not important. I am guessing it would require a new statement/annotation in Zing where you can state "we have now reached line X in file Y from which this file was derived". Like the #line directive in C/C++.

E.g.

Stack trace:
    PRT_VALUE.PrtTupleSet (Main.zing, Line 28905) 
    MACHINE_MainMachine.SendUpdate (Main.zing, Line 3689) [Main.p, Main.SendUpdate, Line 341]
    MACHINE_MainMachine.AnonFun1 (Main.zing, Line 4358) [Main.p, Main.Init.entry, Line 103]
    MACHINE_MainMachine.ReentrancyHelper (Main.zing, Line 3481)
    MACHINE_MainMachine.RunHelper (Main.zing, Line 2464)
    MACHINE_MainMachine.Run (Main.zing, Line 2387)
    MACHINE_MainMachine.Start (Main.zing, Line 2364)

Many built-in assertions in the Zing generated code do not mention the line number where the error occurred in the original P file. E.g.

Error:
P Assertion failed:
Expression: assert(0 <= index && index < size)
Comment: index out of bound

This may be fine for small event handlers, but is very difficult when there are many function calls, etc. and many possible places where the error could have occurred.

Let's do a big scrub across the code base to normalize newlines and replace tab characters with spaces so we stop getting "diff's" that show more changes than were actually made. This needs to be planned at a time when folks don't have big changes they need to merge...

Found by Richard.

At the end of the generated file program.h there is:

PRT_PROGRAMDECL P_GEND_PROGRAM;

This is a definition and so any file that includes program.h is defining its own copy of P_GEND_PROGRAM. "Luckily", most C compilers allow "tentative definitions" and so will treat these as declarations. But C++ compilers do not allow this, so this should fixed to:

extern PRT_PROGRAMDECL P_GEND_PROGRAM;

I was previously getting definitions like the following in program.c:

PRT_TYPE *P_GEND_TYPE_ARTIFACTType = &P_GEND_TYPE_215;

Thus I can refer to the types from the C code easily (by name). I then added another foreign type and these have all disappeared. I am trying to create a test case but I can't get these definitions to appear. I can send you files privately or maybe you can tell what the problem is.

Running build.bat release x64 (and probably all other combinations) currently fails when trying to build the P samples. I think this is because pc no longer outputs program.c and program.h.

• The p.targets file will need to be changed.
• The P sample projects will need to be changed to include different files. Also, if I switch to x64 in VS2015, then some of the P sample projects are still Win32, so this could also be fixed.
• .gitignore will probably need to be updated.

Running with PrtAssert I get 226052 steps per minute and without I get 241069, so PrtAssert is currently costing about 6% which seems a bit high. It would be nice to reduce that cost somehow or make it optional under #if DEBUG flag so we can build a "fast" build when we need one.

One simple optimization is to define PrtAssert like this:

define PrtAssert(c,m) if (!(c)) { _PrtAssert(c,m); }

Inlining the test gives back about 3% of the cost with a minimal binary size increase. Binary size increases from 238337 to 238433, which is only 96 bytes, about 0.04%.

Other improvements could be done by pulling PrtAssert out of any tight loops.

EventDeferredTransDoSameState.txt
Static Error is not detected if the same event is used in “goto” and deferred

• see attached test, lines 24-25 (change file extension from .txt to .p before compiling).
  Note that two other combinations of duplicate events are detected as static errors:
• same event is used in “goto” and “do”
• same event is used in “do” and deferred
  These combinations are also present in the attached test (commented out).

Paul’s work on NodeService exposed a performance problem with excessive cloning in the P runtime. I am noting here a language-level proposal to combat the problem. There are two features I am proposing to add. I am looking for feedback for each feature along three axes: (1) is it useful? (2) is it too restrictive? (3) are there any gotchas?

First, I want to make arguments to functions immutable. If the programmer wants to mutate a parameter, she must make a copy of the parameter into a local variable. With this design, any procedure-local l-value expression passed as an argument to a function call does not have to be cloned; rather the parameter can create an alias. The type checker should disallow global l-value expressions to be passed as a parameter to a function since global variables could be modified anywhere and consequently aliasing would be problematic.

Second, I want to allow a procedure-local l-value expression of a complex type to be passed by reference. If a parameter x is passed by reference, then the contents of x can be mutated (x still cannot be mutated). Of course, this mutation is visible as a side-effect in the caller in the l-value that was passed by reference. The type checker must make sure that only a local variable or a ref parameter l-value is passed as an argument to a function in place of a ref parameter.

Examples:

fun A1(x: int) {
x = 42; // disallowed
}

fun A2(ref x: int) { ... } // disallowed since the type of x is a primitive type

fun A3(ref x: seq[int]) {
x[0] = 42; // allowed
}

fun B(x: seq[int]) {
A3(x); // disallowed
}

fun C() {
var x: seq[int];
x += (0,0);
A3(x); // allowed
assert x[0] == 42; // passes
}

fun D(ref x: seq[int]) {
A3(x); // allowed
}

@clovett @shazqadeer
remove the warnings generated for labels when compiling the C code.

We could add this to the top of every generated program.c file:

pragma warning (disable: 4101)

pragma warning (disable: 4102)

And probably should put this at the bottom of every program.c file to restore back to default for the rest of your app:

pragma warning (default: 4101)

pragma warning (default: 4102)

On master branch. How do I get a hot monitor to cause an error?

See TestMasterHot.p.

event eStart;

main machine MainMachine
{
    start state Init 
    {
        entry 
        {
            monitor eStart;
        }
    }
}

spec M monitors eStart
{
    start hot state Init
    {
        on eStart goto Init;
    }
}

>> load TestMasterHot.p
2s
>> test /liveness
Writing TestMasterHot.zing ...
Compiling TestMasterHot.zing to TestMasterHot.dll ...
7s
>>

D:\pazure\testing3>zinger TestMasterHot.dll -et:et.txt -stats -p:4 /NDFSLiveness

##################
Check Passed
##################
4 distinct states explored
Maximum Depth Explored : 0
Elapsed time : 00:00:00
Memory Stats:
Peak Virtual Memory Size: 560.4453125 MB
Peak Paged Memory Size  : 145.0625 MB
Peak Working Set Size   : 144.09375 MB

D:\pazure\testing3>

I have tried other Zinger liveness flags.

I'm getting P runtime to compile on STM324f chip using GCC, and the generated P output C files contain #pragmas that are Visual Studio cl.exe specific. Would be nice to have a "GCC" option to generate output that compiles cleanly using GCC.

Using pci on modp branch.

I am just executing load and test, but they take a while:

load: 1min40
test: 1min30

So at least 3min10 before I hit the next runtime error due to my mistakes :-)

The name of PrtForeignValueToString does not match the convention of the rest of the foreign type related functions.

PRT_FORGN_MKDEF PrtMkDefaultForeignValue = &MkDefaultForeignValue;
PRT_FORGN_CLONE PrtCloneForeignValue = &CloneForeignValue;
PRT_FORGN_FREE PrtFreeForeignValue = &FreeForeignValue;
PRT_FORGN_GETHASHCODE PrtHashForeignValue = &HashForeignValue;
PRT_FORGN_ISEQUAL PrtIsEqualForeignValue = &IsEqualForeignValue;
PRT_FORGN_TOSTRING PrtForeignValueToString = &ToStringForeignValue;

The use of PrtFreeValue needs to be fixed so as to not accidentally free the value that needs to be cloned due to aliasing.

==PrtValues.c==
PrtTupleSetEx (problem)
PrtSeqUpdateEx (problem)
PrtMapUpdateEx (seems OK – cloning is done upfront)


==PrtExecution.c==
PrtSetGlobalVarEx
PrtSetLocalVarEx

I assume the two above could be a problem if someone does “temp = temp;”?

PrtRaise (probably OK)
PrtPushNewEventHandlerFrame (probably OK)
etc...

I think the rest are probably OK. E.g. I don’t think the runtime will raise an event that is the same instance of the current trigger event!

All my event handlers are functions. This avoids code duplication. Also, the event handlers are quite large and call other functions. But I cannot use raise in a function. So, if I want to use raise, I will have to work around this, perhaps by awkwardly making every function return an event? And then making every event handler check the return value and possibly raise.

I guess the issue is that raise ends execution of the handler. So, if raise was allowed in functions, one would have to assume that every function call could in fact terminate the event handler which would be very strange (kind of like exceptions perhaps?).

But raise is really just (equivalent to) two operations: insert an event at the front of my queue and then return. But we can't access the useful operation (the insert) without having to return. Could we perhaps have the "insert at front of my queue" operation available on its own, without complicating things by forcing a return? This way, I could add an event at the front of my queue from functions without causing any issues or confusion. Otherwise, I can't use this useful (and efficient*) operation (and only because it is stuck to another operation!).

*because, unlike sending an event to myself, it is not a scheduling point, right?

I just changed a few int types to be foreign types and now the compiler hangs. I think we already know about this issue, but I am creating this so we don't forget about it.

I'm getting p-runtime to compile on Nuttx and "PrtWinUser.h" in the generated P code seems too windows specific. Can we genericize that or add option to generate other OS platforms, in my case I want PrtNuttxUser.h... unless you can generalize that - for example, call it "PrtUser.h" and use #ifdef inside that header for any platform specifics...

When a value of type map[any,any] is cast to a variable of type map[int,int] does this involve checking if every key and value present in the map can be cast to int? Or does the cast happen immediately but the next time one reads the map, the cast is done then?

It might be nice to be able to statically get the type of a variable.

E.g.

var MachineList : seq[machine];
...

MachineList = default(typeof(MachineList));

Or allow default to take a variable name instead of a type.

MachineList = default(MachineList);

Should there perhaps be a function PrtGetForeignValue to get the PRT_UINT64 value from a PRT_VALUE* that is a foreign value?

The following warning is worrisome:

Warning 29 warning C4030: first formal parameter list longer than the second list c:\users\qadeer\work\p\src\prtdist\samples\pingpong\program.h 136 1 PingPong

The signatures of generated C code for P functions changed. The foreign functions provided by PrtDist need to reflect that change.

I would like to be able to compare machine values with null. E.g.

assert SomeMachineV == null;

but I get the error:

Values of type machine or interface cannot be compared

Enhancement. It would be nice to have the P line numbers in the generated C code. If you use the #line directive then Visual Studio (or any other debugger) will jump directly to the appropriate line in the P file. You could even step through the P file. This would make seeing which assertion failed much easier.

Some code I am porting uses enums. Something like the following would be nice.

type StatusType = { Invalid, OK, Queued };

type MessageType = (
    Status : StatusType
);

// inside a block

var m : MessageType;

m.Status = StatusType::Invalid;

Or, I could just use int, but then it would be nice to have constants or macros:

let StatusTypeInvalid = 0;
let StatusTypeOK = 1;
let StatusTypeQueued = 2;

type MessageType = (
    Status : int
);

// inside a block

var m : MessageType;

m.Status = StatusTypeInvalid;

The attached program has multiple declarations of the same variable. The error message doesn't point to the location:

multipledef.p (0, 0): same name appears more than once in name tuple or named tuple type
Compilation failed

multipledef.zip

It might be nice to be able to set the output filename(s) from the P compiler. I.e. program.c could be MyPSystem.c. Or, at least, the files could be named the same as the original P file, as is the case with the output zing model. i.e. Main.p -> Main.zing -> Main.dll (on the main branch at least).

The header file generated by the P compiler should have #ifdef __cplusplus just like the runtime header files. Otherwise, from C++ code, you have to do:

// Must include these before including "program.h" otherwise you get errors for having nested extern "C" blocks
#include "PrtWinUser.h"
#include "PrtExecution.h"


extern "C"
{
#include "program.h"
}

When I compile a P program, I am getting some functions in stubs.c like:

void P_DTOR_ServerMachine_IMPL(PRT_MACHINEINST *context)
{
}

but there also some functions declarations in program.h that are not in stubs.c, like:

void P_SEND_OperationManagerMachine_IMPL(PRT_MACHINEINST *context, PRT_VALUE *evnt, PRT_VALUE *payload);

Is this intended?

Also, would this SEND function be executed when a send to this machine occurs (even if this machine has other events in its queue---does this machine have a queue)?

It might be useful to support the string type, even if strings are only used for logging, explaining assertions, etc. A project may require us to call an external logging function with a string argument.

I am trying to run one of my test cases as a C program to debug a potential issue with the C runtime. However, it seems that when P code asks for a fresh foreign value, the runtime just returns 1, 2, 3, etc. My User*Foreign* functions assume these values are pointers and there is no way to distinguish these fake values from real pointers (in theory). So, my program will (almost certainly) crash.

It would be useful to either have a UserMkFreshForeignValue function (which could optionally replace the default). Or, a parameter could be added to most of the User*Foreign* functions so that my code can distinguish between a "fresh" foreign value and a real foreign value. (I'd personally prefer the former.)

I am getting multiple definitions of P_GEND_EVENTSETS in program.c. I can provide the P files.

I'm getting p-runtime to compile on nuttx using GCC and the generated P output contains functions with missing prototypes, and unused variables and unused goto labels. These errors can be avoided by turning off the following compiler features, but I'd prefer not to have to do that because these features are handy way to keep my code clean:

    -Wno-missing-prototypes
    -Wno-missing-declarations
    -Wno-unused-but-set-variable
    -Wno-unused-variable
    -Wno-unused-label

...because it calls the exception handler first and then returns. Also, is there a convenient way to log the exception type?

There are three recent additions in P:

1. Static functions
2. Receive statements
3. Local variables

Need to add regressions for thorough testing of these new features.

We just saw this happen. The actual time was around 50s but the reported time was around 4s. Here is a reminder to look into this.

I think (but I may be wrong) that I will need to use magic numbers when accessing the values of named tuple types from foreign code.

This will be very hard to maintain if the tuple types change (in the P code). Also, I think I will be converting large, nested tuple types to structs and back quite a lot, so I will no doubt make some mistakes.

It looks like the structure of named tuples can be explored/discovered/confirmed at runtime. But there is no way to get rid of the magic numbers. Ideally, I would like something like this:

    temp = PrtTupleGet(payload, _NT_INDEX_SettingsType_Id);
    // ...
    temp = PrtTupleGet(payload, _NT_INDEX_SettingsType_Message);


    temp = PrtTupleGet(temp, _NT_INDEX_HelloMessageType_Data);
    temp = PrtTupleGet(temp, _NT_INDEX_HelloDataType_Name);

assuming the following types in P (although there could be additional fields added at any time):

type SettingsType =
(
  Id : int,
  Message : HelloMessageType
);

type HelloMessageType = 
(
  Data : HelloDataType
);

type HelloDataType =
(
  Name : int
);

On modp branch.

Edit:

• Allow interfaces in sends, receives and po declarations to denote a set of events.
• Allow e.g. the following: po ITesterMachine > IReceiverMachine;.

Old:
I can use interfaces in po declarations, but then zing fails to compile it. I have a non-minimal example if it would help. (Of course, it would be nice if this was actually supported! But right now I guess it is supposed to be a compile error!)

The following causes a KeyNotFoundException when generating the zing model.

crash.p:

module MyModule
{

main machine Manager {


    start state Init
    {
        entry
        {
            send this, halt;
        }
    }

}
}

test crash: MyModule;
implementation MyModule;

D:\pazure\testing>pc crash.p
Writing stubs.c ...
Writing program.h ...
Writing program.c ...

Unhandled Exception: System.Collections.Generic.KeyNotFoundException: The given key was not present in the dictionary.
   at System.Collections.Generic.Dictionary`2.get_Item(TKey key)
   at Microsoft.Pc.PToZing.TypeTranslationContext.ConstructType(FuncTerm type) in d:\pazure\P\Src\Pc\Compiler\PToZing.cs:line 4263
   at Microsoft.Pc.PToZing.TypeTranslationContext.PTypeToZingExpr(FuncTerm pType) in d:\pazure\P\Src\Pc\Compiler\PToZing.cs:line 4256
   at Microsoft.Pc.PToZing.FoldNulApp(FuncTerm ft, IEnumerable`1 children, ZingFoldContext ctxt) in d:\pazure\P\Src\Pc\Compiler\PToZing.cs:line 3273
   at Microsoft.Pc.PToZing.ZingFold(ZingFoldContext ctxt, Node n, IEnumerable`1 children) in d:\pazure\P\Src\Pc\Compiler\PToZing.cs:line 2855
   at Microsoft.Pc.PToZing.<>c__DisplayClass53.<MkZingFunMethod>b__52(Node x, IEnumerable`1 ch) in d:\pazure\P\Src\Pc\Compiler\PToZing.cs:line 3956
   at Microsoft.Formula.API.ASTComputation`1.Compute()
   at Microsoft.Formula.API.ASTConcr`1.Compute[S](Func`2 unfold, Func`3 fold, CancellationToken cancel)
   at Microsoft.Pc.PToZing.MkZingFunMethod(String machineName, String funName, FunInfo funInfo) in d:\pazure\P\Src\Pc\Compiler\PToZing.cs:line 3954
   at Microsoft.Pc.PToZing.GenerateMachineClass(String machineName) in d:\pazure\P\Src\Pc\Compiler\PToZing.cs:line 2080
   at Microsoft.Pc.PToZing.MkZingClasses(List`1 elements) in d:\pazure\P\Src\Pc\Compiler\PToZing.cs:line 2098
   at Microsoft.Pc.PToZing.GenerateZing(List`1& FileNames, AST`1& outModel) in d:\pazure\P\Src\Pc\Compiler\PToZing.cs:line 1687
   at Microsoft.Pc.Compiler.GenerateZing(List`1 flags) in d:\pazure\P\Src\Pc\Compiler\Compiler.cs:line 412
   at Microsoft.Pc.Compiler.Compile(String inputFileName, List`1& flags) in d:\pazure\P\Src\Pc\Compiler\Compiler.cs:line 378
   at Microsoft.Pc.Compiler.Compile(String inputFileName) in d:\pazure\P\Src\Pc\Compiler\Compiler.cs:line 42
   at Microsoft.Pc.CommandLine.Main(String[] args) in d:\pazure\P\Src\Pc\CommandLine\CommandLine.cs:line 85

When compiling a test case to C, I get a read access violation. I believe the currentState field of PRT_MACHINEINST_PRIV is a garbage value, but I could be wrong. It could be a bug in Prt or in the generated code. I am not sure how to debug this. Can Visual Studio do reverse debugging? 😄

Branch: modp.

event eReq;

module Manager
{
    main machine DriverMachine
    {
        start state Init {

            entry (p : int) {
            }
            // line 13:
            on eReq do (p : int) {
            };
        }

    }
}

test manager: Manager;
implementation Manager;

When compiling the above, I get the following error.

d:/pazure/testing/issue1.p (13, 4): Payload type for event must be subtype of payload type of do function;

It would be useful to be able to concatenate two seq values together.

E.g.

var s1 : seq[machine];
var s2 : seq[machine];
// ...


s1 = s1 + s2;

Currently, I have to do:

index = 0;
while(index < sizeof(s2))
{
  s1 += (sizeof(s1), s2[index]);
  index = index + 1;
}

...which I think is right.
...except my variable names are much longer than s1 and s2!

I am thinking about dropping the inferred types from golden output of the regression tests. I find there is a lot of noise there that needs to be sifted through whenever I make a change to the compiler. Any opinions?

Sometimes P compiler generates a p_tmp_params field that is not used, this generates an error from GCC compiler. One can disable that error, but I'd prefer not to do that.

GCC complains if a C function has no prototype. One can disable that error my adding -Werror=missing-prototypes, but I'd prefer not to do that. One easy solution would be to add the keyword "static" at the beginning of the function which declares that this function is internal to the module, which it is in our case.