The Coq mailing list

[Andrew Appel <appel AT CS.Princeton.EDU>]

Dear Coq team:

I am pleased to report that Coq 8.5pl1 has good performance

compared to Coq 8.4pl6.  It's generally (but not always) faster,

and it consistently uses only half as much memory.

I ported the Verified Software Toolchain to Coq 8.5pl1.  

Then I measured the VST's verification of a C program,

OpenSSL's SHA-256 cryptographic hashing (see here.)

This verification is 9857 lines of Coq spread over 23 files.

(I do not include the hundreds of .v files in the VST itself, 

only the files for applying VST to this C program.)

I measured its performance on my very fast desktop computer

(Intel core i7-4770 @ 3.4 GHz, running 64-bit Windows 7).  

Normally I do "make -j" to run 8 threads in parallel to check this proof,

but for this measurement I ran single-threaded.  I am using a 32-bit Coq,

whose maximum Ocaml virtual memory size is 2 gigabytes.

In Coq 8.4pl6 it takes 1934 seconds, In Coq 8.5pl1 it takes 1789 seconds,

about 7% faster.   This scatterplot is quite interesting:

Each dot represents one of my .v files.  As you can see,

sometimes 8.5pl1 is twice as fast, sometimes 8.4pl6 is twice as fast.

As time permits, I will investigate which specific parts of the proof

are slower in 8.5pl1, and isolate them for the Coq team.

Coq 8.5pl1 uses half as much memory!  Two representative examples:

	8.4pl6 time (sec)	8.5pl1 time (sec)	8.4pl6 space (MB)	8.5pl1 space (MB)
verif_sha_init	97.4	54.9	692.8	322.2+43.2
verif_sha_bdo8	159.3	361.9	925.9	400.2+00.0

As you can see, whether 8.5pl1 is twice as fast or half as fast, it still takes only half

the memory.  

What does 322.2+43.2 mean?

For 8.4pl6, the number given here for MB (megabytes) is Working Set.

For 8.5pl1, it is reported as X+Y, where X is Working Set and

Y=(Commit Charge - Working Set).  "Commit Charge" is total virtual address

space used; "Working Set" is actual pages regularly touched.  I didn't report (+Y)

for 8.4pl6 because Y=0 in that case.  I believe that the difference in Y may be related

to the new version of Ocaml used to compile 8.5pl1:  that version (sometimes?)

reserves a substantial part of the address space for some purpose.

Overall, I congratulate the Coq development team for the improvements

to performance from Coq 8.4 to Coq 8.5.

Sincerely,

Andrew Appel

Attachment: 50186.3
Description: PNG image