Sing# verifier

Nov 16, 2008 at 10:56 AM
Hi,

I'm glad to see that SDK 2.0 is out!

I want to run Sing# verifier.
As I guess it's singver.exe.

When I try to run it, I receive the message:

Unhandled Exception: System.IO.FileLoadException: The located assembly's manifest definition with name 'mllib10'
does not match the assembly reference.
File name: "mllib10"
at Test._main()

=== Pre-bind state information ===
LOG: DisplayName = mllib10, Version=1.0.9.11, Culture=neutral, PublicKeyToken=a19089b1c74d0809
(Fully-specified)
LOG: Appbase = C:\user\Singularity\base\build\
LOG: Initial PrivatePath = NULL
Calling assembly : singver, Version=0.0.0.0, Culture=neutral, PublicKeyToken=null.
===

LOG: Private path hint found in configuration file: fsc.
LOG: Publisher policy file is not found.
LOG: Host configuration file not found.
LOG: Using machine configuration file from c:\WINDOWS\Microsoft.NET\Framework\v1.1.4322\config\machine.config.
LOG: Post-policy reference: mllib10, Version=1.0.9.11, Culture=neutral, PublicKeyToken=a19089b1c74d0809
LOG: Attempting download of new URL file:///C:/user/Singularity/base/build/mllib10.DLL.
WRN: Comparing the assembly name resulted in the mismatch: Minor Version


The manifest of singver.exe contains following lines:

...

.assembly extern fslib10
{
.publickeytoken = (A1 90 89 B1 C7 4D 08 09 ) // .....M..
.ver 1:0:9:11
}
.assembly extern mllib10
{
.publickeytoken = (A1 90 89 B1 C7 4D 08 09 ) // .....M..
.ver 1:0:9:11
}
.assembly extern absil10
{
.publickeytoken = (3B 73 4F 0D 5C 10 D3 2E ) // ;sO.\...
.ver 1:0:9:11
}

...

As you can see, singver requires 1.0.9.11 version of fslib10, mllib10 and absil10.
In RDK 2.0 these files has 1.9.2.11 version.
Is it possible to post Sing# verifier compatible with 1.9.2.11 version?
Or upload 1.0.9.11 version of required files?

Thank you.


Coordinator
Nov 17, 2008 at 10:32 PM
Hi mortalis, thanks for your interest in the RDK. The Sing# verifier is out-of-date - it has not been maintained and there are not currently plans to fix it. I'm afraid you won't be able to use this tool, and it will be removed in a subsequent update. However, many properties of contracts are verified by the sgc compiler at build time. Let me know if you have any other questions.
--
Derrick Coetzee
Microsoft Research Operating Systems Group developer

Nov 19, 2008 at 11:14 AM
Edited Nov 20, 2008 at 7:29 AM
Thanks for answer.

Here some more questions I want to ask:

1. sgc compiler has option /verify. When I try to run sgc with this option, I receive the message:

error CS2651: Plugin type 'Microsoft.Boogie.BoogiePlugin' does not implement interface Microsoft.SpecSharp.IPlugin

Actually interface Microsoft.SpecSharp.IPlugin has only one method CreateVisistor and type Microsoft.Boogie.BoogiePlugin implements it.
What's the matter?

2.One another option is /verifyopt:<option list>. What options could be in <option list>?
Coordinator
Nov 22, 2008 at 11:18 AM
Hi mortalis. These options are from the internal desktop version of Sing#, and are not applicable to Singularity. If you're interested in exploring more of the verifications capabilities of Sing#, I suggest trying the public Spec# release, which is similar to Sing# but without the contract support:

http://research.microsoft.com/specsharp

We're also planning to include source code and binaries from a more recent version of Sing# in the RDK in a future incremental release, so stay tuned if you're interested in that. Hope this helps, let me know if you have any other questions.
--
Derrick Coetzee
Microsoft Research Operating Systems Group developer

Nov 25, 2008 at 9:13 AM

Hi Derrick.

Especially I'm intresting in contract verification, so Spec# is not so interesting for me as Sing#.

In post above you mentioned that sgc compiler verify many properties of contracts at build time.

Which properties are verified? Which properties must be verified, but not verified? What conditions must contract satisfy to pass verfication?

Nov 25, 2008 at 5:30 PM
Edited Nov 25, 2008 at 5:31 PM
Isn't that what Spec# is?  The main difference with Sing# is the addition of channels and low level programming extensions, or so I thought.  Spec# adds contracts, pre and post-condition and object invariants and has the boogie verifier.
Coordinator
Nov 25, 2008 at 9:47 PM
jclary: There's some confusion over ambiguous use of the term "contracts" here. There's contracts in the sense of pre- and post-conditions and object invariants, which Spec# does support; but there's also the contracts using the contract keyword that were added by Sing# to specify channel interfaces. You might call them channel contracts. These are something completely different.

mortalis: I've asked the designer of Sing#, Manuel Fahndrich, about your question and he or I will get back to you.
--
Derrick Coetzee
Microsoft Research Operating Systems Group developer
Nov 25, 2008 at 10:29 PM
I just looked through SDN17, the design note for Sing# and I noticed that the description of contracts (Section 2.1) is quite out of date in that it contains some early design that we subsequently restricted quite a bit. There is a small note in Section 2.1.2 to this effect, but it means that much of the following description is really pointless:

[NOTE: Currently, Sing# only allows the "one" form of states and does not permit mixed send/receive alternatives]

I will update it when possible. Let me spell out the current restrictions on channel contracts, what's implemented in the compiler, and what possible bugs there seem to lurk.

The Sing# compiler should enforce the following rules on channel contracts.
  1. No mixed send/receive states: The set next actions in a state should either be all sends, or all receives, but not a mixture thereof. The Sing# compiler should reject contracts with such states. However, it seems that the released sgc has a regression in that it does not issue an error for such states.
  2. No send cycles: To preallocate all channel memory and thus make channels space bounded, the compiler checks that there are no cycles in the state diagrams consisting of all sends or all receives, as this would enable one side of the channel to continously send and unbounded amount of data.
  3. No recursion through sub-states. When using sub-states in the state machine, there must exist a stratification of sub-states, such that a state can only invoke substates at a lower level, thereby avoiding recursions.
The above rules (in particular 1) by construction should rule out deadlocks on a single channel. Deadlock can still arise if processes communicate with multiple channels.

Contract extensions: The rules explained in 2.1.7 in SDN17 seem to be accurate.

Endpoint checking:
The Sing# compiler enforces rules on how code can handle channel endpoints. Channel endpoints live in the exchange heap and are thus restricted to be owned by a single thread at any given time. The compiler enforces this by treating endpoint references linearly. See section 2.5 of SDN17.

Other information:
  • The state annotations on endpoints (of the form C.Exp:State) that is allowed in method signatures and in type instantiations, is currently not enforced either at compile- or runtime.
  • The channel conformity of code (using channel endpoints only with appropriate messages in appropriate states) is currenlty checked only at runtime. The static verification is possible and was prototyped several years ago in the form of the singver verifier. However, it has not been maintained.
  • Downcasts of channels: when using channel with inheritance, downcasts are possible at runtime. The downcast only checks the channel type, but not the channel state, even if the state is specified.

Hope this helps,

-MaF

Jul 17, 2009 at 3:05 AM

"The static verification is possible and was prototyped several years ago in the form of the singver verifier. However, it has not been maintained."

I am really interested in this verifier.  Is there any documentation available somewhere?  I have only read several paper but they only scuffed the surface.  This topic falls directly in my research area. 

What I really want to know is how the data passed with a message is/was handled by the verifier.  This data is important since the code most likely depends on this data; which also affects the possible send/receive operations.  Therefore, was all the possible values systematically checked by the verifier. eg.  If a message is received along with an int, was all values checked whenever the endpoint is in a state where that message may be received?  Maybe the verifier was using some technique using a satisfiability prover?  Or maybe, the verifier could identify false positives by overlooking the values??

Any information would be greatly appreciated! 

Thank you

 

Jul 29, 2009 at 11:45 PM

Hi,

The protocol verification did not depend on any values of message parameters, only message type.

-MaF

From: moozphat [mailto:notifications@codeplex.com]
Sent: Thursday, July 16, 2009 7:06 PM
To: Manuel Fahndrich
Subject: Re: Sing# verifier [singularity:40031]

From: moozphat

"The static verification is possible and was prototyped several years ago in the form of the singver verifier. However, it has not been maintained."

I am really interested in this verifier. Is there any documentation available somewhere? I have only read several paper but they only scuffed the surface. This topic falls directly in my research area.

What I really want to know is how the data passed with a message is/was handled by the verifier. This data is important since the code most likely depends on this data; which also affects the possible send/receive operations. Therefore, was all the possible values systematically checked by the verifier. eg. If a message is received along with an int, was all values checked whenever the endpoint is in a state where that message may be received? Maybe the verifier was using some technique using a satisfiability prover? Or maybe, the verifier could identify false positives by overlooking the values??

Any information would be greatly appreciated!

Thank you

Read the full discussion online.

To add a post to this discussion, reply to this email (singularity@discussions.codeplex.com)

To start a new discussion for this project, email singularity@discussions.codeplex.com

You are receiving this email because you subscribed to this discussion on CodePlex. You can unsubscribe on codePlex.com.

Please note: Images and attachments will be removed from emails. Any posts to this discussion will also be available online at codeplex.com