Donald Sebastian Leung (Jun 05 2021 at 07:22): 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)?
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.
Donald Sebastian Leung (Jun 05 2021 at 08:52):Interesting read, thanks for sharing!
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.)
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. :)
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: Oct 13 2024 at 01:02 UTC