Boogie generates error warnings when executing CIVL Inductive Sequentialization Tests

[prpr2770]

I am currently obtaining the following errors/output on the terminal, for the test-cases contained within Tests/civl/InductiveSequentialization:

// 2PC.bpl

Prover error: line 15 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 16 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 13 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 14 column 20: invalid sort parameter, symbol or ')' expected
Boogie program verifier finished with 72 verified, 0 errors

// BroadcastConsensus.bpl

Prover error: line 15 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 18 column 49: unknown sort 'T@PA'
Prover error: line 13 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 16 column 49: unknown sort 'T@PA'

Boogie program verifier finished with 29 verified, 0 errors

// ChangRoberts.bpl

Prover error: line 15 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 18 column 29: unknown sort 'T@PA'
Prover error: line 13 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 16 column 29: unknown sort 'T@PA'

Boogie program verifier finished with 41 verified, 0 errors

// ChangRoberts_pendingAsyncs.bpl

Prover error: line 15 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 16 column 46: unknown sort 'T@PA'
Prover error: line 13 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 14 column 46: unknown sort 'T@PA'

Boogie program verifier finished with 46 verified, 0 errors

//Gauss.bpl

Prover error: line 15 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 16 column 49: unknown sort 'T@PA'
Prover error: line 13 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 14 column 49: unknown sort 'T@PA'

Boogie program verifier finished with 8 verified, 0 errors

//NBuyer.bl

Prover error: line 15 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 16 column 47: unknown sort 'T@PA'
Prover error: line 13 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 14 column 47: unknown sort 'T@PA'

Boogie program verifier finished with 130 verified, 0 errors

//NoChoice.bpl

Prover error: line 15 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 17 column 37: unknown sort 'T@PA'
Prover error: line 13 column 20: invalid sort parameter, symbol or ')' expected

Boogie program verifier finished with 8 verified, 0 errors

// PingPong.bpl

Prover error: line 15 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 19 column 37: unknown sort 'T@PA'
Prover error: line 13 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 17 column 37: unknown sort 'T@PA'

Boogie program verifier finished with 45 verified, 0 errors

// ProducerConsumer.bpl

Prover error: line 15 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 19 column 37: unknown sort 'T@PA'
Prover error: line 13 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 17 column 37: unknown sort 'T@PA'

Boogie program verifier finished with 28 verified, 0 errors

// paxos/is.sh

Prover error: line 16 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 17 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 14 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 15 column 20: invalid sort parameter, symbol or ')' expected

Boogie program verifier finished with 116 verified, 0 errors

// paxos/ref.sh

Prover error: line 16 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 17 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 14 column 20: invalid sort parameter, symbol or ')' expected
Prover error: line 15 column 20: invalid sort parameter, symbol or ')' expected

Boogie program verifier finished with 30 verified, 0 errors

[bkragl]

Are you using the latest Boogie and Z3 4.8.8? Because with that I don't see any errors (neither locally on my machine nor in our CI). I can also generate the SMT-LIB files and run Z3 directly without seeing any errors.

boogie 2PC.bpl /proverLog:2PC.smt2
z3 2PC.smt2

[prpr2770]

I'm sorry, I guess that's the issue. The versions I'm using are:

1. z3 : v4.4.1 ( installed using sudo apt-get install z3 on Ubuntu 18.04.6 LTS)
2. boogie : v2.11.2.0

[prpr2770]

I'm new to boogie and civl, and I'm really interested to learn how to apply inductive sequentialization to new problems. I shall try out the examples in the paper and check the example scripts provided. It'd really help if there's some tutorial that's developed, to guide one, in learning how to write multiple-layered concurrent programs in civl.

Additionally, I understand that unlike civl, Armada (which is built on top of Dafny, which can feed input into boogie) has the provision of connecting different programs of the sequential refinement procedure, using proof scripts. Also, it has support for weak memory models. Are you aware of support for inductive sequentialization in Armada, or support for weak memory models in civl?

[shazqadeer]

Try these links: https://civl-verifier.github.io/ https://civl-verifier.github.io/doc

As far as I know, Armada does not support inductive sequentialization.

There is no native support for weak memory models in Civl; the user has to model weak memory manually with appropriate encoding using buffers etc.

[prpr2770]

Thank you for the pointers. I have attempted to create a documentation for two simple test-scripts within the Test/civl/InductiveSequentialization folder and I'd like to share them with you all. Would it be possible for me to have a meeting/discussion with the authors, and improve on the documentation, so that we can share it publicly in the repository? The draft version of the documentation are linked below as gists:

1. PingPong
2. ChangRoberts

In particular, I've some queries/concerns from reading the paper and exploring the code of the examples:

1. Each ATOMIC-ACTION is assigned a MOVER-TYPE. Is that assignment handled manually or automatically? What if a given thread has both send and recv atomic actions witthin it? In our-case, each atomic Procedure has a mover-type, but it comprises of both send and recv. How do we determine the mover-type of each procedure?
2. What are non-movers?
3. How does adding a constraint for CollectAbs make it non-blocking, and thus a left-mover?
4. What does havoc do?
5. What does assume {:add_to_pool "INV1", k, k+1} {:add_to_pool "PInit", PInit(n)} pid(k) || k == 0; mean in ChangRoberts.bpl ?

[shazqadeer]

Answers to questions:

1. The mover type of an atomic action is specified by the user. You should see annotations like the following: {:left}, {:right}, {:both}, {:atomic}, in the source files.
2. Non-movers are atomic actions that are neither left nor right movers. These actions are annotated with {:atomic}.
3. I will respond separately after refreshing my memory about CollectAbs.
4. havoc is a Boogie command that assigns arbitrary values to its arguments, e.g., havoc x, y; will put arbitrary values into x and y.
5. These annotations are a new feature for quantifier instantiation. This feature is new and has minimal documentation in CommandLineOptions.cs. I will try to add more. You can get a sense of how this feature works by looking at the samples in Test/inst/ folder.

Would it be possible for me to have a meeting/discussion with the authors, and improve on the documentation, so that we can share it publicly in the repository?

I am happy to discuss with you. Send me a message. We will find a time. Which repository do you want to share your documentation in?

[shazqadeer]

Answer for the CollectAbs question (#3 above):

Collect is blocking because of this statement which needs at least n messages in CH[i]: vs := receive(n) CH[i]

The two guards added in CollectAbs are as follows:

assert forall j. Broadcast(j) \not \in \Omega assert |CH[i]| ≥ n

The second guard will fail if there are fewer than n messages in CH[i]. This means that either CollectAbs fails or it will proceed all the way to the end. Therefore, it satisfies the definition of nonblocking.

Next, we talk about why CollectAbs is a left mover. To make this argument, we must show that CollectAbs commutes to the left of Main, Broadcast, and Collect. The argument for Main and Collect is based on linear permissions whose discussion is elided in the PLDI paper but is visible in the code file Test/civl/inductive-sequentialization/BroadcastConsensus.bpl (the proof in the code file is somewhat different from that presented in the paper). The argument for commuting to the left of Broadcast is based on the first guard. If Broadcast(j) executes(for some j) followed by CollectAbs(i), then Broadcast(j) \in \Omega in the starting state which means that CollectAbs(i) will fail when executed in that state. This shows that CollectAbs(i) commutes to the left of Broadcast(j).

[prpr2770]

Thank you @shazqadeer for the detailed response to my queries. I shall drop you a message via email, to schedule a meeting. I was thinking of including the *.md documentation files, in the same folder as the associated *.bpl script files, within boogie/Test/civl/* folders.

[prpr2770]

5. These annotations are a new feature for quantifier instantiation. This feature is new and has minimal documentation in CommandLineOptions.cs.  I will try to add more.  You can get a sense of how this feature works by looking at the samples in Test/inst/ folder.

I just noticed that the CommandLineOptions.cs you indicated , is located at: /Source/ExecutionEngine/CommandLineOptions.cs. I'm not really familiar with the codebase and hence, I'm uncertain of how this may be used.

I shall discuss the queries that I have regarding the Test/civl/inductive-sequentialization/BroadcastConsensus.bpl in out meeting.

[shazqadeer]

Closing since @prpr2770 and I have connected offline and will continue to discuss Civl and inductive sequentialization.