This is the topic to ask questions on the talk "Towards an Axiomatic Basis for C++".
Talk just started!
By not supporting uninstantiated templates, do you mean that the user must specify and prove each instantiation of a template separately?
Question: What is currently an example of a killer feature of Iris or Coq that makes it possible what you are doing, and what killer feature of Iris or Coq are you missing that would make your work significantly easier?
I have been working with a postdoc of mine on a similar front-end based on clang to convert code written in a subset of C into a clean AST representation. We used the ClangML tool (https://github.com/Antique-team/clangml), which offers an OCaml representation of Clang AST; do you? My project aims at applying verified source-to-source optimizations (transformation guided by the programmer, but applied by a tool); are you also interested in source-to-source optimizations?
(1) What is your model of C++? Is it a language model? Is it a model of clang's C++?
Have you been comparing notes with the Frama/Clang plugin for Frama-C?
(2) How big are your separation logic rules for C++ statements?
Many thanks for the interesting talk - I will give it a try!
robbert said:
Question: What is currently an example of a killer feature of Iris or Coq that makes it possible what you are doing, and what killer feature of Iris or Coq are you missing that would make your work significantly easier?
@Gregory Malecha I would be curious to know the long list of killer features you mentioned you would like (both of Iris and of Coq).
Same here ;)
We looked at Frama-C early on, but decided to go this route instead. It would be interesting to compare notes on where we are though.
Jean Pichon said:
(2) How big are your separation logic rules for C++ statements?
our theories directory is ~9k that isn't all axioms though
How did you validate your model of C++? (It seems like a huge task…)
(apparently I don't know how to respond to thing appropriately)
We have a simple instantiation of the separation logic assertions that we provide (e.g. the identity
predicate that you saw, as well as points to and such). We don't attempt to prove the wp rules because we do not have an underlying operational model of C++ to verify it against. Even if we did, it isn't obvious (to me) that an operational model of C++ would be much more trustworthy than our axiomatic one
You didn't say anything about what code has actually been verified?
Can you give a sense of what kind of things you can verify, and what kind of things you can't verify? And do you need assumptions?
At the moment, we've finished verifications of some concurrent and non-concurrent data structures. locks, finite maps, etc. I wouldn't say that any of that part of the verification is especially novel at this point, but we have built some interesting specifications for our hypervisor in iris and are working on the verification of those
...and the underlying memory object model?
Frama-C converts C++ to C. We decided not to do that and allow direct reasoning about C++. During proofs, it is probaby easier to look at the code as written rather than transformed code (C++ to C).
we don't need assumptions outside of the axioms that are in the repository, though to be completely honest, we do occasionally admit arithmetic lemmas that are unpleasant to prove (though we do go back and fill in the holes)
Regarding the axiomatic vs. operational model question, cross-validation between the two would be one way to bring confidence, but I appreciate that might not be on your critical path. Also, an executable operational model can be validated by running it; do you have a way to check pre- and post-condition pairs against executions (by evaluating
simple pre- and post-conditions)?
Peter Sewell said:
...and the underlying memory object model?
In our simple instantiation, our object memory model is quite close to what exists in CompCert, though the wp rules avoid exposing it at that level of detail. We've found that in most cases, we don't need to fall back on things like offsets and instead rely on a type "Loc" (which is in the development) of locations. So we might write somtehing like _local r "x" ., _field foo ., _field bar
to compute x.foo.bar
We've done some work on verification of device drivers as well, e.g., UARTs.
Jean Pichon said:
(2) How big are your separation logic rules for C++ statements?
theories/lang/cpp/logic/stmt.v is ~340 lines, but some things like destructors have been broken out into separate files
@Arthur Charguéraud : do you have a link to your source-to-source optimizations project?
Gregory Malecha said:
Jean Pichon said:
(2) How big are your separation logic rules for C++ statements?
theories/lang/cpp/logic/stmt.v is ~340 lines, but some things like destructors have been broken out into separate files
How big is the rule for an assignment, for example?
Hello. In one of your slides, you presented typing management and especially inheritance, with a general type and an optional most derived type. Considering a typing situation like in the following picture, how would you represent the T
type? Do you have two instances of the predicate, one with A
as general type and A2
as most derived one, and another one with B
as general type and B2
as most derived one? Sorry if the question looks very simple, beginner student here. Thanks in advance! t.png
robbert said:
robbert said:
Question: What is currently an example of a killer feature of Iris or Coq that makes it possible what you are doing, and what killer feature of Iris or Coq are you missing that would make your work significantly easier?
Gregory Malecha I would be curious to know the long list of killer features you mentioned you would like (both of Iris and of Coq).
We're able to work around a lot of things but some things that would be nice are
Require Import
is fairly slow in some of our code, e.g. Require Import bedrock.lang.auto.cpp
(not included in the distribution) takes around 4 seconds which seems like a lot. Just Require Import iris...
can take a second or two.Gordon Stewart said:
We've done some work on verification of device drivers as well, e.g., UARTs.
What did you prove about UART? Do you have a spec of the protocol?
And how to you model talking with devices?
Jean Pichon said:
Gregory Malecha said:
Jean Pichon said:
(2) How big are your separation logic rules for C++ statements?
theories/lang/cpp/logic/stmt.v is ~340 lines, but some things like destructors have been broken out into separate files
How big is the rule for an assignment, for example?
Assignment is actually an expression in C++. The rule are here: https://github.com/bedrocksystems/cpp2v/blob/master/theories/lang/cpp/logic/expr.v#L245
Regarding 5., it could be interesting to split the Require
and Import
to measure which one is slow.
Maxime Dénès said:
Regarding 5., it could be interesting to split the
Require
andImport
to measure which one is slow.
Thanks. I'll take a look at that.
Enzo Crance said:
Hello. In one of your slides, you presented typing management and especially inheritance, with a general type and an optional most derived type. Considering a typing situation like in the following picture, how would you represent the
T
type? Do you have two instances of the predicate, one withA
as general type andA2
as most derived one, and another one withB
as general type andB2
as most derived one? Sorry if the question looks very simple, beginner student here. Thanks in advance! t.png
It works something like this, let's just simplify to class T : public A , public B
and suppose that you have a this : ptr
which represents the pointer to T
. Then you would have something like the following:
this |-> _identity "T" (Some "T") **
this ., _base "T" "A" |-> _identity "A" (Some "T") **
this ., _base "T" "B" |-> _identity "B" (Some "T")
Gregory Malecha said:
Jean Pichon said:
Gregory Malecha said:
Jean Pichon said:
(2) How big are your separation logic rules for C++ statements?
theories/lang/cpp/logic/stmt.v is ~340 lines, but some things like destructors have been broken out into separate files
How big is the rule for an assignment, for example?
Assignment is actually an expression in C++. The rule are here: https://github.com/bedrocksystems/cpp2v/blob/master/theories/lang/cpp/logic/expr.v#L245
Thanks! (I hadn't noticed the .v files were also available. I took the README too literally.)
Gregory Malecha said:
Peter Sewell said:
...and the underlying memory object model?
In our simple instantiation, our object memory model is quite close to what exists in CompCert, though the wp rules avoid exposing it at that level of detail. We've found that in most cases, we don't need to fall back on things like offsets and instead rely on a type "Loc" (which is in the development) of locations. So we might write somtehing like
_local r "x" ., _field foo ., _field bar
to computex.foo.bar
Do you have a feeling and/or some experimental data of how the CompCert object layout model and the clang object layout model relate?
Jean Pichon said:
Regarding the axiomatic vs. operational model question, cross-validation between the two would be one way to bring confidence, but I appreciate that might not be on your critical path. Also, an executable operational model can be validated by running it; do you have a way to check pre- and post-condition pairs against executions (by evaluating
simple pre- and post-conditions)?
It may be possible to skip operational semantics entirely: it may be possible to write a compiler from C++ to CompcertC and prove that the compiler preserves the axiomatic semantics (e.g. using VST as the target axiomatic semantics). Does anyone know previous work trying this approach (preservation of axiomatic semantics) to compiler verification?
Jean Pichon said:
Gordon Stewart said:
We've done some work on verification of device drivers as well, e.g., UARTs.
What did you prove about UART? Do you have a spec of the protocol?
And how to you model talking with devices?
We built an operational model of a standard UART (ARM's PL011) and verified a trace-style spec of the driver code against the operational model. We used a variant of Iris's STSs to connect the trace spec to the device model.
Abhishek Anand said:
Jean Pichon said:
Regarding the axiomatic vs. operational model question, cross-validation between the two would be one way to bring confidence, but I appreciate that might not be on your critical path. Also, an executable operational model can be validated by running it; do you have a way to check pre- and post-condition pairs against executions (by evaluating
simple pre- and post-conditions)?It may be possible to skip operational semantics entirely: it may be possible to write a compiler from C++ to CompcertC and prove that the compiler preserves the axiomatic semantics (e.g. using VST as the target axiomatic semantics). Does anyone know previous work trying this approach (preservation of axiomatic semantics) to compiler verification?
Is that something you want to do for your project? Writing a C++ compiler is a daunting endeavour.
Jean Pichon said:
Gregory Malecha said:
Peter Sewell said:
...and the underlying memory object model?
In our simple instantiation, our object memory model is quite close to what exists in CompCert, though the wp rules avoid exposing it at that level of detail. We've found that in most cases, we don't need to fall back on things like offsets and instead rely on a type "Loc" (which is in the development) of locations. So we might write somtehing like
_local r "x" ., _field foo ., _field bar
to computex.foo.bar
Do you have a feeling and/or some experimental data of how the CompCert object layout model and the clang object layout model relate?
Currently, we know of the CompCert model and the model that @robbert wrote in his dissertation. He can probable give you a better description of the difference than I can. Our current simple_pred.v
instantiates with a model that is close to CompCert, but I believe that our rules would be compatible (or close to compatible with) with the model in @robbert 's thesis though I can't guarantee that.
Gordon Stewart said:
Jean Pichon said:
Gordon Stewart said:
We've done some work on verification of device drivers as well, e.g., UARTs.
What did you prove about UART? Do you have a spec of the protocol?
And how to you model talking with devices?We built an operational model of a standard UART (ARM's PL011) and verified a trace-style spec of the driver code against the operational model. We used a variant of Iris's STSs to connect the trace spec to the device model.
Nice! :-)
Jean Pichon said:
Abhishek Anand said:
Jean Pichon said:
Regarding the axiomatic vs. operational model question, cross-validation between the two would be one way to bring confidence, but I appreciate that might not be on your critical path. Also, an executable operational model can be validated by running it; do you have a way to check pre- and post-condition pairs against executions (by evaluating
simple pre- and post-conditions)?It may be possible to skip operational semantics entirely: it may be possible to write a compiler from C++ to CompcertC and prove that the compiler preserves the axiomatic semantics (e.g. using VST as the target axiomatic semantics). Does anyone know previous work trying this approach (preservation of axiomatic semantics) to compiler verification?
Is that something you want to do for your project? Writing a C++ compiler is a daunting endeavour.
Writing a compiler isn't on the short list, but we are interested in this sort of thing in the long run (or integrating with some existing verified compiler).
Jean Pichon said:
Gordon Stewart said:
Jean Pichon said:
Gordon Stewart said:
We've done some work on verification of device drivers as well, e.g., UARTs.
What did you prove about UART? Do you have a spec of the protocol?
And how to you model talking with devices?We built an operational model of a standard UART (ARM's PL011) and verified a trace-style spec of the driver code against the operational model. We used a variant of Iris's STSs to connect the trace spec to the device model.
Nice! :-)
This works, but building an operational model, even of a simple device, is a lot of work. I'd love pointers on ways to re-use existing models. I know that people in Cambridge have ported models of ARM chips to tools like Sail; is there any existing work that does something similar but for peripheral devices?
Gordon Stewart said:
Jean Pichon said:
Gordon Stewart said:
Jean Pichon said:
Gordon Stewart said:
We've done some work on verification of device drivers as well, e.g., UARTs.
What did you prove about UART? Do you have a spec of the protocol?
And how to you model talking with devices?We built an operational model of a standard UART (ARM's PL011) and verified a trace-style spec of the driver code against the operational model. We used a variant of Iris's STSs to connect the trace spec to the device model.
Nice! :-)
This works, but building an operational model, even of a simple device, is a lot of work. I'd love pointers on ways to re-use existing models. I know that people in Cambridge have ported models of ARM chips to tools like Sail; is there any existing work that does something similar but for peripheral devices?
@Peter Sewell
Gregory Malecha said:
Jean Pichon said:
Abhishek Anand said:
Jean Pichon said:
Regarding the axiomatic vs. operational model question, cross-validation between the two would be one way to bring confidence, but I appreciate that might not be on your critical path. Also, an executable operational model can be validated by running it; do you have a way to check pre- and post-condition pairs against executions (by evaluating
simple pre- and post-conditions)?It may be possible to skip operational semantics entirely: it may be possible to write a compiler from C++ to CompcertC and prove that the compiler preserves the axiomatic semantics (e.g. using VST as the target axiomatic semantics). Does anyone know previous work trying this approach (preservation of axiomatic semantics) to compiler verification?
Is that something you want to do for your project? Writing a C++ compiler is a daunting endeavour.
Writing a compiler isn't on the short list, but we are interested in this sort of thing in the long run (or integrating with some existing verified compiler).
What do you use in the meantime? Clang?
And if so, have you thought of connecting with Vellvm?
Jean Pichon said:
Gregory Malecha said:
Jean Pichon said:
Abhishek Anand said:
Jean Pichon said:
Regarding the axiomatic vs. operational model question, cross-validation between the two would be one way to bring confidence, but I appreciate that might not be on your critical path. Also, an executable operational model can be validated by running it; do you have a way to check pre- and post-condition pairs against executions (by evaluating
simple pre- and post-conditions)?It may be possible to skip operational semantics entirely: it may be possible to write a compiler from C++ to CompcertC and prove that the compiler preserves the axiomatic semantics (e.g. using VST as the target axiomatic semantics). Does anyone know previous work trying this approach (preservation of axiomatic semantics) to compiler verification?
Is that something you want to do for your project? Writing a C++ compiler is a daunting endeavour.
Writing a compiler isn't on the short list, but we are interested in this sort of thing in the long run (or integrating with some existing verified compiler).
What do you use in the meantime? Clang?
And if so, have you thought of connecting with Vellvm?
We compile with both gcc and clang at this point. Because we're so close to the source it isn't too big of a problem to use a different compiler. We aren't relying on any clang internal transformations (though of course parsing / type checking bugs would impact things), though it is an extra bit of untrusted code.
Vellvm is probably the best way for us to get to a verified compiler at the moment, I've talked with @Yannick Zakowski about it, but we haven't gone much farther than informal conversations at this point.
I appreciate all the questions. If you have any more, feel free to ask them in the github project or send me an email: gregory@bedrocksystems.com
Thanks! It's really interesting work, and it seems quite challenging, so best of lucks! :-)
I don't know of work on real behavioural models of devices. The ETH folk (David Cock and others?) have done some SoC modelling, but AFAIK only more abstractly.
Last updated: Dec 07 2023 at 06:38 UTC