Stream: Coq users

Topic: Proving absence of memory leak in Verifiable C


view this post on Zulip Donald Sebastian Leung (Jun 05 2021 at 07:22):

I have been recently going through Volume 5 of Software Foundations on Verifiable C and encountered malloc() and free() in the third chapter. The specification of free() takes a pointer with an associated malloc_token in the precondition and "disposes" of it, presumably freeing the memory under the pointer; however, according to my understanding, a function that takes in such a pointer and does nothing would also satisfy this specification (correct me if I am wrong). If so, does that mean that there is no easy way to prove that a particular C program is free of memory leaks using VST (alone)?

view this post on Zulip Paolo Giarrusso (Jun 05 2021 at 08:30):

VST is a linear logic, so there's no immediate way to throw away resources. However, @Ralf Jung has written on this https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf#page92

In personal conversation, we got confirmation that this [a certain use of impredicative invariants] is likely sufficient to “leak” resources in VST, in the same vein as Theorem 2. And indeed, VST does not have a theorem stating that memory-leak freedom can be established by showing a Hoare triple with postcondition Emp.

view this post on Zulip Donald Sebastian Leung (Jun 05 2021 at 08:52):

Interesting read, thanks for sharing!

view this post on Zulip Ralf Jung (Jun 05 2021 at 09:19):

a function that takes in such a pointer and does nothing would also satisfy this specification (correct me if I am wrong)

If it does literally nothing, I think it might not be possible to satisfy the spec. But if it creates a lock and is creative about making the lock invariant self-referential, I think it is possible to satisfy the free spec without actually freeing anything. (That's what I referred to in the quote above.)

view this post on Zulip Ralf Jung (Jun 05 2021 at 09:20):

I haven't literally tried to do this in Coq though as that I am not a VST expert. Could be a fun exercise for someone with more VST knowledge. :)

view this post on Zulip Ralf Jung (Jun 05 2021 at 09:37):

see in particular https://www.cs.princeton.edu/~appel/papers/hobor.pdf#page=92, the "unlock" rule -- which has postcondition emp


Last updated: Jan 29 2023 at 03:28 UTC