PLDI'15 demo for Termite

Config : Linux sorlin 3.13.0-45-generic #74-Ubuntu SMP Tue Jan 13 19:36:28 UTC 2015 x86_64 x86_64 x86_64 GNU/Linux

Date : vendredi 13 février 2015, 19:39:50 (UTC+0100)

Loopus

Name Logs Files Terminate Don't know Time Rate

polybench loopus_polybench.json 30 30 0 28 ms 100%

sortsExp loopus_sortsExp.json 6 3 3 55 ms 50%

termcomp loopus_termcomp.json 129 78 51 16 ms 60%

wtc loopus_wtc.json 7 4 3 227 ms 57%

Termite

Name Logs Files Terminate Don't know Errors LP Time Rate

polybench termite_polybench.json 30 21 9 0 (10, 3) 71 ms 70%

sortsExp termite_sortsExp.json 6 5 1 0 (15, 4) 85 ms 83%

termcomp termite_termcomp.json 134 118 12 4 (2, 1) 9 ms 88%

wtc termite_wtc.json 65 46 12 7 (4, 2) 15 ms 70%

Rank

Name Logs Files Terminate Don't know Errors LP Time Rate

wtc rank_wtc.json 44 32 10 2 (513, 204) 52 ms 72%

Aprove

Name Logs Files Terminate Don't know Time Rate

polybench aprove_polybench.json 30 0 30 1364 ms 0%

sortsExp aprove_sortsExp.json 6 0 6 9431 ms 0%

termcomp aprove_termcomp.json 135 108 27 9889 ms 80%

wtc aprove_wtc.json 65 27 38 7322 ms 41%

	Rank
wtc	rank_wtc.json	44	32	10	2	(513, 204)	52 ms	72%

Column "Files" : number of files of the given benchmark for which an intermediate representation is generated by the front-end.
Columns "Time" average wall time per analysed file.
(Rank and Termite) Columns "LP" : average size (lines, columns) of the Linear Programming instances.
C2FSM (Rank's frontend) is not robust enough to parse other benchmarks than WTC.
T2 is not part of the comparison since the C-front-end is not yet maintained.
We did not manage to launch TAN, we got many errors while processing C-files and the tool is not documented.