Stream: wg-secure-code

Topic: proving things


nikomatsakis (Oct 29 2018 at 17:04, on Zulip):

Hey @RalfJ and maybe others:

I have a question. I am working on salsa some in my spare time, which is a re-implementation of the incremental infrastructure from the compiler. It uses some read-write locks and a bit of error-prone logic that I've already gotten wrong a few times -- basically I have to reason about "all possible interleavings" which is hard to do. After the latest bug, I wanted to try and get more systematic in my approach. I can try to work this out on pen+paper (and probably will), but I was wondering if there is a nice "lightweight" tool that would let me try to encode the states I think and help me to reason about the interleavings. It feels like something that I ought to be able to use... I don't know ... Coq for or something. =)

nikomatsakis (Oct 29 2018 at 17:04, on Zulip):

I put this in this area because this feels like the sort of thing secure code might also want to do...

nikomatsakis (Oct 29 2018 at 17:04, on Zulip):

...I know for Rayon I've often wanted to do similar things, though in that case I am reasoning about unsafe code, which makes things all the more fun.

nikomatsakis (Oct 29 2018 at 17:05, on Zulip):

oh hey I see a similar topic correctness proofs...

RalfJ (Oct 29 2018 at 18:34, on Zulip):

if you ask me I'll tell you you don't want to think about interleavings. instead you want to think about ownership, in the sense of separation logic. :D

RalfJ (Oct 29 2018 at 18:35, on Zulip):

reasoning about concurrent code by looking at interleavings is like reasoning about sequential code by considering assembly-level details like registers. it works, if you are willing to suffer, but you really ought to work with a higher-level abstraction if you can (and most of the time, you can).

RalfJ (Oct 29 2018 at 18:37, on Zulip):

but unfortunately I don't know much about tools for doing this kind of reasoning. If you want to do it in Coq, sure, there are some frameworks you can use (and I am author of one of them), but that's pretty complex stuff and takes a long time to get into

RalfJ (Oct 29 2018 at 18:38, on Zulip):

there are some tools but I am not deeply familiar with any of them

RalfJ (Oct 29 2018 at 18:38, on Zulip):

but what about asking in the wg-verification gitter at https://gitter.im/rust-lang/wg-verification ? some of these tools' authors are there :P

nikomatsakis (Oct 29 2018 at 18:55, on Zulip):

if you ask me I'll tell you you don't want to think about interleavings. instead you want to think about ownership, in the sense of separation logic. :D

You're not wrong about this, and it is kind of what I've been doing -- I basically want to show that the "ownership model" I have in my head is correctly implemented, I guess.. I have to think about it. To be honest talking about "tools" is the wrong thing, I should start by just writing in English the protocol which I'm sure will help 100x

RalfJ (Oct 29 2018 at 19:19, on Zulip):

bonus points if you use separation logic instead of English :)

Last update: Nov 11 2019 at 22:25UTC