modelchecking/writecache

P primer

Examples

writecache/ contains simple shard + writecache implementation.

An example of replaying buggy schedule:

$ p check -r writecache_0_0.schedule -v .
.. Searching for a P compiled file locally in the current folder
.. Found a P compiled file: /repo/modelchecking/writecache/PGenerated/CSharp/net6.0/writecache.dll
Replay option is used, checker is ignoring all other parameters and using the writecache_0_0.schedule to replay the schedule
... Replaying writecache_0_0.schedule
.. Test case :: tcSingleClient
... Checker is using 'replay' strategy.
<TestLog> Running test 'tcSingleClient'.
<CreateLog> DeleteIsFinal was created.
<MonitorLog> DeleteIsFinal enters state 'Init'.
<StateLog> TestWithSingleClient(2) enters state 'Init'.
<CreateLog> Metabase(3) was created by TestWithSingleClient(2).
<CreateLog> Blobstor(4) was created by TestWithSingleClient(2).
<CreateLog> Shard(5) was created by TestWithSingleClient(2).
<PrintLog> <AnnounceLog> 'TestWithSingleClient(2)' announced event 'eSpec_DeleteIsFinal_Init'.
<MonitorLog> DeleteIsFinal is processing event 'eSpec_DeleteIsFinal_Init' in state 'Init'.
<MonitorLog> DeleteIsFinal exits state 'Init'.
<MonitorLog> DeleteIsFinal enters state 'WaitForAnOp'.
<CreateLog> Client(6) was created by TestWithSingleClient(2).
<StateLog> Shard(5) enters state 'Init'.
<StateLog> Client(6) enters state 'Init'.
<GotoLog> Client(6) is transitioning from state 'Init' to state 'DoSomething'.
<StateLog> Client(6) exits state 'Init'.
<StateLog> Client(6) enters state 'DoSomething'.
<MonitorLog> DeleteIsFinal is processing event 'eShardReqPut with payload (<source:Client(6), obj:<address:0, obj:0, >, >)' in state 'WaitForAnOp'.
<StateLog> Blobstor(4) enters state 'Init'.
<StateLog> Metabase(3) enters state 'Init'.
<SendLog> 'Client(6)' in state 'DoSomething' sent event 'eShardReqPut with payload (<source:Client(6), obj:<address:0, obj:0, >, >)' to 'Shard(5)'.
<ReceiveLog> Client(6) is waiting to dequeue an event of type 'eShardResPut' or 'PHalt' in state 'DoSomething'.
<CreateLog> Cache(7) was created by Shard(5).
<GotoLog> Shard(5) is transitioning from state 'Init' to state 'WorkLoop'.
<StateLog> Shard(5) exits state 'Init'.
<StateLog> Shard(5) enters state 'WorkLoop'.
<DequeueLog> 'Shard(5)' dequeued event 'eShardReqPut with payload (<source:Client(6), obj:<address:0, obj:0, >, >)' in state 'WorkLoop'.
<StateLog> Cache(7) enters state 'Init'.
<GotoLog> Cache(7) is transitioning from state 'Init' to state 'FlushLoop'.
<StateLog> Cache(7) exits state 'Init'.
<StateLog> Cache(7) enters state 'FlushLoop'.
<SendLog> 'Shard(5)' in state 'WorkLoop' sent event 'eCacheReqPut with payload (<source:Shard(5), obj:<address:0, obj:0, >, >)' to 'Cache(7)'.
<ReceiveLog> Shard(5) is waiting to dequeue an event of type 'eCacheResPut' or 'PHalt' in state 'WorkLoop'.
<DequeueLog> 'Cache(7)' dequeued event 'eCacheReqPut with payload (<source:Shard(5), obj:<address:0, obj:0, >, >)' in state 'FlushLoop'.
<PrintLog> PUT address=0
<SendLog> 'Cache(7)' in state 'FlushLoop' sent event 'eCacheResPut with payload (<address:0, >)' to 'Shard(5)'.
<ReceiveLog> 'Shard(5)' dequeued event 'eCacheResPut with payload (<address:0, >)' and unblocked in state 'WorkLoop'.
<SendLog> 'Cache(7)' in state 'FlushLoop' sent event 'eFlushSingle' to 'Cache(7)'.
<SendLog> 'Shard(5)' in state 'WorkLoop' sent event 'eMetaReqUpdateId with payload (<source:Shard(5), address:0, storageId:0, >)' to 'Metabase(3)'.
<ReceiveLog> Shard(5) is waiting to dequeue an event of type 'eMetaResUpdateId' or 'PHalt' in state 'WorkLoop'.
<DequeueLog> 'Metabase(3)' dequeued event 'eMetaReqUpdateId with payload (<source:Shard(5), address:0, storageId:0, >)' in state 'Init'.
<DequeueLog> 'Cache(7)' dequeued event 'eFlushSingle' in state 'FlushLoop'.
<PrintLog> Start FLUSH, address=0
<SendLog> 'Metabase(3)' in state 'Init' sent event 'eMetaResUpdateId with payload (<address:0, >)' to 'Shard(5)'.
<ReceiveLog> 'Shard(5)' dequeued event 'eMetaResUpdateId with payload (<address:0, >)' and unblocked in state 'WorkLoop'.
<MonitorLog> DeleteIsFinal is processing event 'eShardResPut with payload (<address:0, >)' in state 'WaitForAnOp'.
<SendLog> 'Shard(5)' in state 'WorkLoop' sent event 'eShardResPut with payload (<address:0, >)' to 'Client(6)'.
<ReceiveLog> 'Client(6)' dequeued event 'eShardResPut with payload (<address:0, >)' and unblocked in state 'DoSomething'.
<SendLog> 'Cache(7)' in state 'FlushLoop' sent event 'eBlobReqPut with payload (<source:Cache(7), obj:<address:0, obj:0, >, >)' to 'Blobstor(4)'.
<ReceiveLog> Cache(7) is waiting to dequeue an event of type 'eBlobResPut' or 'PHalt' in state 'FlushLoop'.
<MonitorLog> DeleteIsFinal is processing event 'eShardReqDel with payload (<source:Client(6), address:0, >)' in state 'WaitForAnOp'.
<SendLog> 'Client(6)' in state 'DoSomething' sent event 'eShardReqDel with payload (<source:Client(6), address:0, >)' to 'Shard(5)'.
<ReceiveLog> Client(6) is waiting to dequeue an event of type 'eShardResDel' or 'PHalt' in state 'DoSomething'.
<DequeueLog> 'Shard(5)' dequeued event 'eShardReqDel with payload (<source:Client(6), address:0, >)' in state 'WorkLoop'.
<DequeueLog> 'Blobstor(4)' dequeued event 'eBlobReqPut with payload (<source:Cache(7), obj:<address:0, obj:0, >, >)' in state 'Init'.
<SendLog> 'Blobstor(4)' in state 'Init' sent event 'eBlobResPut with payload (<address:0, storageId:42, >)' to 'Cache(7)'.
<ReceiveLog> 'Cache(7)' dequeued event 'eBlobResPut with payload (<address:0, storageId:42, >)' and unblocked in state 'FlushLoop'.
<SendLog> 'Shard(5)' in state 'WorkLoop' sent event 'eBlobReqDel with payload (<source:Shard(5), address:0, >)' to 'Blobstor(4)'.
<ReceiveLog> Shard(5) is waiting to dequeue an event of type 'eBlobResDel' or 'PHalt' in state 'WorkLoop'.
<DequeueLog> 'Blobstor(4)' dequeued event 'eBlobReqDel with payload (<source:Shard(5), address:0, >)' in state 'Init'.
<SendLog> 'Blobstor(4)' in state 'Init' sent event 'eBlobResDel with payload (<address:0, >)' to 'Shard(5)'.
<ReceiveLog> 'Shard(5)' dequeued event 'eBlobResDel with payload (<address:0, >)' and unblocked in state 'WorkLoop'.
<SendLog> 'Shard(5)' in state 'WorkLoop' sent event 'eMetaReqDelete with payload (<source:Shard(5), address:0, >)' to 'Metabase(3)'.
<ReceiveLog> Shard(5) is waiting to dequeue an event of type 'eMetaResDelete' or 'PHalt' in state 'WorkLoop'.
<DequeueLog> 'Metabase(3)' dequeued event 'eMetaReqDelete with payload (<source:Shard(5), address:0, >)' in state 'Init'.
<SendLog> 'Metabase(3)' in state 'Init' sent event 'eMetaResDelete with payload (<address:0, >)' to 'Shard(5)'.
<ReceiveLog> 'Shard(5)' dequeued event 'eMetaResDelete with payload (<address:0, >)' and unblocked in state 'WorkLoop'.
<SendLog> 'Cache(7)' in state 'FlushLoop' sent event 'eMetaReqUpdateId with payload (<source:Cache(7), address:0, storageId:42, >)' to 'Metabase(3)'.
<ReceiveLog> Cache(7) is waiting to dequeue an event of type 'eMetaResUpdateId' or 'PHalt' in state 'FlushLoop'.
<MonitorLog> DeleteIsFinal is processing event 'eShardResDel with payload (<address:0, >)' in state 'WaitForAnOp'.
<DequeueLog> 'Metabase(3)' dequeued event 'eMetaReqUpdateId with payload (<source:Cache(7), address:0, storageId:42, >)' in state 'Init'.
<SendLog> 'Metabase(3)' in state 'Init' sent event 'eMetaResUpdateId with payload (<address:0, >)' to 'Cache(7)'.
<ReceiveLog> 'Cache(7)' dequeued event 'eMetaResUpdateId with payload (<address:0, >)' and unblocked in state 'FlushLoop'.
<PrintLog> Finish FLUSH, address=0, remaining=0
<SendLog> 'Shard(5)' in state 'WorkLoop' sent event 'eShardResDel with payload (<address:0, >)' to 'Client(6)'.
<ReceiveLog> 'Client(6)' dequeued event 'eShardResDel with payload (<address:0, >)' and unblocked in state 'DoSomething'.
<SendLog> 'Client(6)' in state 'DoSomething' sent event 'eShardReqExists with payload (<source:Client(6), address:0, >)' to 'Shard(5)'.
<ReceiveLog> Client(6) is waiting to dequeue an event of type 'eShardResExists' or 'PHalt' in state 'DoSomething'.
<DequeueLog> 'Shard(5)' dequeued event 'eShardReqExists with payload (<source:Client(6), address:0, >)' in state 'WorkLoop'.
<SendLog> 'Shard(5)' in state 'WorkLoop' sent event 'eMetaReqExists with payload (<source:Shard(5), address:0, >)' to 'Metabase(3)'.
<ReceiveLog> Shard(5) is waiting to dequeue an event of type 'eMetaResExists' or 'PHalt' in state 'WorkLoop'.
<DequeueLog> 'Metabase(3)' dequeued event 'eMetaReqExists with payload (<source:Shard(5), address:0, >)' in state 'Init'.
<SendLog> 'Metabase(3)' in state 'Init' sent event 'eMetaResExists with payload (<address:0, found:True, storageId:42, >)' to 'Shard(5)'.
<ReceiveLog> 'Shard(5)' dequeued event 'eMetaResExists with payload (<address:0, found:True, storageId:42, >)' and unblocked in state 'WorkLoop'.
<MonitorLog> DeleteIsFinal is processing event 'eShardResExists with payload (<address:0, found:True, >)' in state 'WaitForAnOp'.
<ErrorLog> Assertion Failed: PSpec/GetCorrect.p:41:9
<StrategyLog> Found bug using 'replay' strategy.
Error: Assertion Failed: PSpec/GetCorrect.p:41:9
... Emitting verbose logs:
..... Writing PCheckerOutput/BugFinding/writecache_0_verbose.trace.json
... Reproduced 1 bug.
... Elapsed 0.2006418 sec.~~ [PTool]: Thanks for using P! ~~