coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Andrew Appel <appel AT CS.Princeton.EDU>
To: coq-club AT inria.fr
Subject: [Coq-Club] VST 2.5x faster under Coq 8.6
Date: Fri, 17 Mar 2017 08:18:47 -0400 (EDT)
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=appel AT CS.Princeton.EDU; spf=Pass smtp.mailfrom=appel AT cs.princeton.edu; spf=None smtp.helo=postmaster AT yellowcard.cs.princeton.edu
Ironport-phdr: 9a23:r/BRqhau+gveiBbnijBsoHH/LSx+4OfEezUN459isYplN5qZpsu5bnLW6fgltlLVR4KTs6sC0LuL9f66EjdbqdbZ6TZZL8wKD0dEwewt3CUeQ+e9QXXhK/DrayFoVO9jb3RCu0+BDE5OBczlbEfTqHDhpRQbGxH4KBYnbr+tQt2a3IyL0LW5/ISWaAFVjhK8Z6lzJVO4t1b/rM4T1KJkJrw81VPgumNFf6wCzHtwKFa7tC263t2x+pVu7yNW/d8NypgTAu3BY60kQOkAX3wdOGcv6ZizuA==

Dear Coq Club:

I am happy to report that the Verified Software Toolchain is now

ported to Coq 8.6, and runs about 2.5x faster than it did in Coq 8.5.

What "runs" is the Floyd proof automation system doing separation

logic proofs in Coq; Floyd is a mix of Ltac and reflective (computational)

proof. "Small" proofs don't run faster, but some things that were really

really really slow are now just really slow, for a substantial improvement.

I expected this result, since my experiments with "new universes"

in Coq 8.5 last year predicted a 2x performance improvement, but

I am glad to measure it in Coq 8.6. Recall also that last year I reported

that VST ran 2x faster in Coq 8.5 than it did in Coq 8.4, so this

is excellent sustained improvement by the Coq team.

There were two obstacles to the port, described in bug reports

5225 and 5379, but we found workarounds to those, as described

in the "additional comments" of the bug reports.

Memory use of Coq 8.6 vs Coq 8.5 seems to be the same.

We find that 32-bit Coq runs VST more than twice as fast as 64-bit Coq.

(These measurements were in Coq 8.5 but I expect the same would

hold in Coq 8.6.) Normally, 32-bit x86_64 does not run faster than

64-bit x86_64 code, but in this case (where we have 1-gigabyte images

even in 32-bit mode), there may be important cache locality effects

in the Ocaml system and garbage collector. Therefore, it's still important

to support a performant 32-bit Coq.

-- Andrew Appel