In doing VST verifications of application software, one may want to call upon library functions that have standard specifications. The VSTlib provides these in the style of "Verified Software Units". For an introduction to VSUs, see the second half of Software Foundations Volume 5: Verifiable C.
Each component of VSTlib is envisioned to have a single header file (something.h), which may be a standard system header file such as math.h or a VSTlib-specific version such as SC_atomics.h. Each component has one or more .c files which must be linked with the application c files; linking of .o files is done with the standard system linker and is not foundationally verified. In the VSU library, linking is foundationally theorized at the level of Clight abstract syntax, with proofs.
Each VSTlib component may be external and axiomatized (such as the mmap system call), or constructed and proved (such as the memmgr construction of (subset of) the standard malloc/free interface.
The following VSUs are included now or envisioned. Header files listed with in boldface are standard system headers from /usr/include; the others are in VSTlib's include directory.
| Name | header | ASI | VSU | P/A | Done? | Comments |
|---|---|---|---|---|---|---|
| math | math.h | spec_math.MathASI | verif_math.MathVSU | Axiomized | mostly | see below |
| memmgr | memmgr.h | Proved | soon | custom, verified allocator | ||
| malloc | stdlib.h | spec_malloc.MallocASI | verif_malloc.MallocVSU | Axiomatized | Done | standard system allocator |
| atomics | stdatomic.h, SC_atomics.h | spec_SC_atomics.AtomicsASI | verif_SC_atomics.SCAVSU | Axiomatized | Done | atomic load, store, CAS, etc. |
| locks | threads.h, VSTthreads.h | spec_locks.LockASI | verif_locks.lockVSU | Proved | Done | busy-wait locks based on atomics |
| threads | threads.h, VSTthreads.h | spec_threads.ThreadsASI | verif_threads.ThreadsVSU | Proved | Done |
Additional details:
-
math: Each function in the system standard math.h library can be axiomatized with (1) special preconditions as needed, such as that the argument of sqrt must be nonnegative in order to guarantee any accuracy bounds; and (2) relative and absolute error bounds, which need not be the default bounds for the given floating-point type. (That is, the
sinfunction might have more than 1 ulp of error.) All the functions are axiomatized, but many of the error bounds are not reliable; we plan to update the error bounds based on the GNU documentation. Also, thelong doublefunctions are not supported. -
memmgr: This is the "Verified Sequential Malloc/Free" published by Naumann and Appel.
-
malloc: This is an axiomatized version of standard Posix malloc/free, for those users who want to call the standard library implementations.
opam repository add coq-released
opam install coq-vst-lib
- For C include files, add to your CFLAGS:
-I $(OPAM_SWITCH_PREFIX)/lib/coq/user-contrib/VSTlib/include - For C sources to compile and link with:
$(OPAM_SWITCH_PREFIX)/lib/coq/user-contrib/VSTlib/src - Within Coq:
From VSTlib Require Import spec_malloc.(* etc *)
(Instead of opam, you could build from sources and do make install, and adjust your paths to `lib/coq/user-contrib' appropriately.)
Example clients that demonstrate how to use these VSUs can be found in the VSTlib/test directory; see test/README.md.