mirror of
https://github.com/AdaCore/spark2014.git
synced 2026-02-12 12:39:11 -08:00
222 lines
12 KiB
ReStructuredText
222 lines
12 KiB
ReStructuredText
=====================
|
|
Tools and Performance
|
|
=====================
|
|
|
|
Tools used
|
|
===========
|
|
The following tools were used:
|
|
|
|
- GNATprove 0.2w (20130414)
|
|
- GPS 5.3.0w (20130415)
|
|
- GNAT Pro 7.2.0w (20130414-47)
|
|
- SPARK Pro toolset 11.0.0
|
|
|
|
Performance
|
|
===========
|
|
The results reported in this section are from analysis on a desktop PC
|
|
(i7 860, 2.8GHz, 4 CPUs, 6Gb RAM) running 64-bit Linux (Debian).
|
|
|
|
The timings for GNATprove were generated by running "Clean Proofs" followed by
|
|
"Prove Subprogram" from within GPS and noting the elapsed time reported in the
|
|
Messages tab. It is acknowledged that these times include the time spent by
|
|
GNATprove analysing and generating VCs as well as the time spent by Alt-Ergo
|
|
attempting to discharge the VCs, plus any additional overhead from GPS.
|
|
|
|
The SPARK 2005 timings were generated by running the command "time spadesimp subprog.vcg"
|
|
and taking the reported 'real' time on the assumption that this is closest to the
|
|
measure reported by GPS. (The Simplifier executable is called spadesimp.)
|
|
It is acknowledged that this does not include the time spent by the Examiner analysing
|
|
and generating VCs, although this has been measured separately and is only 00.15s in total
|
|
for all seven subprograms in the fisr example (Exchange).
|
|
|
|
For GNATprove (SPARK 2014) the option -j4 was used to specify 4 parallel processes to make
|
|
use of the available processors. For SPARKsimp (SPARK 2005) the equivalent option -p=4 was
|
|
used.
|
|
|
|
Exchange procedure
|
|
==================
|
|
|
|
================================ ================== ================== ========
|
|
Subprogram GNATprove SPARK 2005 Comments
|
|
================================ ================== ================== ========
|
|
Exchange Proved 00.56s Proved 00.08s
|
|
Exchange_No_Post Proved 00.30s Proved 00.08s
|
|
Exchange_No_Post_Unused Proved 00.35s Proved 00.08s
|
|
Exchange_No_Post_Uninitialized Proved 00.35s Not proved 00.08s 1
|
|
Exchange_With_Post_Unused Not proved 01.55s Not proved 00.09s 2
|
|
Exchange_With_Post_Uninitialized Not proved 01.47s Not proved 00.10s 2
|
|
Exchange_RTE Not proved 01.77s Not proved 00.11s 2
|
|
================================ ================== ================== ========
|
|
|
|
Comments:
|
|
|
|
#. Uninitialized variable results in unprovable (false) VCs in SPARK 2005. This is detected by
|
|
GNATprove when run in flow analysis mode.
|
|
|
|
#. VCs not provable due to deliberate error. GNATprove timings reflect the 1s timeout used.
|
|
|
|
Stacks, Queues and QueueOperations
|
|
==================================
|
|
|
|
================================ ================== ================== ========
|
|
Subprogram GNATprove SPARK 2005 Comments
|
|
================================ ================== ================== ========
|
|
ReverseQueue Proved 00.40s Proved 00.08s
|
|
================================ ================== ================== ========
|
|
|
|
Stacks, Queues and QueueOperations with Proof
|
|
=============================================
|
|
|
|
================================ ================== ================== ========
|
|
Subprogram GNATprove SPARK 2005 Comments
|
|
================================ ================== ================== ========
|
|
ReverseQueue Proved 06.06s Proved 00.59s 1
|
|
================================ ================== ================== ========
|
|
|
|
Comments:
|
|
|
|
#. The timeout for GNATprove was increased to 2s for this example. The SPARK 2005
|
|
time consists of 0.516s for the Simplifier to prove 25 out of 27 VCs and 0.069s
|
|
for Victor + Alt-Ergo to prove the remaining 2 VCs.
|
|
|
|
Central Heating Controller
|
|
==========================
|
|
|
|
RTE Proof
|
|
---------
|
|
|
|
================================ ================== ================== ========
|
|
Subprogram GNATprove SPARK 2005 Comments
|
|
================================ ================== ================== ========
|
|
HeatingSystem_DFA Proved 02.79s Proved 01.71s
|
|
================================ ================== ================== ========
|
|
|
|
Correctness Proof
|
|
-----------------
|
|
|
|
================================ ================== ================== ========
|
|
Subprogram GNATprove SPARK 2005 Comments
|
|
================================ ================== ================== ========
|
|
HeatingSystem_Proof Proved 08.41s Proved 02.64s 1
|
|
================================ ================== ================== ========
|
|
|
|
Comments:
|
|
|
|
#. There were 97 SPARK 2005 VCs of which 96 were proved by the Simplifier and the
|
|
remaining one was proved by Victor + Alt-Ergo. GNATprove generated and proved
|
|
37 VCs.
|
|
|
|
Advanced SPARK 2005 Training Course
|
|
===================================
|
|
|
|
================================ ================== ================== ========
|
|
Subprogram GNATprove SPARK 2005 Comments
|
|
================================ ================== ================== ========
|
|
Increment Proved 00.61s Proved 00.14s
|
|
Increment2 Proved 00.88s Proved 00.17s
|
|
Swap, NandGate, NextDay_* (t1q3) Proved 01.32s Proved 00.55s 1
|
|
Swap, NandGate, NextDay_* (alt) Proved 01.32s Proved 00.46s
|
|
ISQRT Proved 02.18s Proved 00.29s
|
|
Bounded_Add Proved 01.12s Proved 00.34s 2
|
|
Raise_To_Power Not proved Not proved 3
|
|
================================ ================== ================== ========
|
|
|
|
Comments:
|
|
|
|
#. These are the combined times for proving all the subprograms named as they are all
|
|
located in the same package. (Timings for individual subprograms could be obtained
|
|
by using 'Prove Subprogram' with GNATprove and by proving the individual VC files
|
|
with the SPARK 2005 tools if this information was required.) GNATprove generates
|
|
and discharges checks for four postconditions and a range check. The SPARK 2005
|
|
tools generate and discharge 24 VCs of which 23 are discharged by the Simplifier
|
|
and the remaining one requires Victor + Alt-Ergo.
|
|
|
|
#. Of the 15 SPARK 2005 VCs, 14 were discharged by the Simplifier and 1 by Victor + Alt-Ergo.
|
|
|
|
#. Come back to this - open todo item in main body of report.
|
|
|
|
Array Examples
|
|
==============
|
|
|
|
================================ ================== ================== ========
|
|
Subprogram GNATprove SPARK 2005 Comments
|
|
================================ ================== ================== ========
|
|
T2Q1.Swap Proved 00.56s Proved 00.20s
|
|
T2Q2.Clear Proved 00.51s Proved 00.16s
|
|
T2Q3.Find Proved 00.51s Proved 00.17s 1
|
|
T2Q4.Clear Proved 02.63s Proved 00.42s 2
|
|
T2Q5.MaxElement_P1B1 Proved 01.52s Proved 00.27s
|
|
T2Q5.MaxElement_P2B1 Not proved 03.09s Proved 00.53s
|
|
T2Q5.MaxElement_P3B1 Proved 00.86s Proved 00.10s 4
|
|
T2Q5.MaxElement_P1B2 Proved 01.62s Proved 00.38s
|
|
T2Q5.MaxElement_P2B2 Not proved 03.29s Proved 00.83s 3
|
|
T2Q5.MaxElement_P3B2 Proved 01.11s Proved 00.12s
|
|
T2Q5.MaxElement_P1B3 Proved 01.72s Proved 00.31s
|
|
T2Q6.SumArray Proved 11.08s Proved 00.40s 5
|
|
T2Q6.SumArray_Shift Proved 09.37s Proved 00.80s 5
|
|
T2Q7.Find Proved 01.08s Proved 00.23s
|
|
T2Q8.CreateFibArray Not proved 13.42s Not proved 16.62s
|
|
T2Q8.CreateFibArray_RTCOnly Not proved 13.20s Not proved 16.40s
|
|
================================ ================== ================== ========
|
|
|
|
#. T2Q3 is not mentioned in the body of the report as it is identical to T2Q7 but without
|
|
a postcondition.
|
|
|
|
#. Of the 9 SPARK 2005 VCs, 7 were discharged by the Simplifier and 2 by Victor + Alt-Ergo.
|
|
|
|
#. See observation and explanation in main body of report.
|
|
|
|
#. In fact GNATprove does not generate or prove any VCs as this example is so trivial.
|
|
|
|
#. The GNATprove timeout was increased to 12s.
|
|
|
|
Further Advanced SPARK course examples
|
|
======================================
|
|
|
|
================================ ================== ================== ========
|
|
Subprogram GNATprove SPARK 2005 Comments
|
|
================================ ================== ================== ========
|
|
T3Q1.Swap and Rotate3 (combined) Proved 01.32s Proved 00.39s 1
|
|
T3Q2.Double and Quadruple Proved 01.27s Proved 00.29s
|
|
T3Q3.DoNothing Not proved 03.70s Not proved 1m49s
|
|
T3Q4.SumArray Proved 04.60s Proved 00.45s 2
|
|
T3Q5.* (Sorting algorithm) Not proved 10.92s Proved 20.22s 3
|
|
================================ ================== ================== ========
|
|
|
|
#. Of the 8 SPARK 2005 VCs 7 were proved by the Simplifier and 1 by Victor + Alt-Ergo.
|
|
|
|
#. Of the 6 SPARK 2005 VCs 4 were proved by the Simplifier and 2 by Victor + Alt-Ergo.
|
|
|
|
#. There were 32 SPARK 2005 VCs. 24 were proved by the Simplifier, 1 requiring a user-defined
|
|
rule. The remainder were discharged by Victor + Alt-Ergo.
|
|
|
|
Tokeneer
|
|
========
|
|
|
|
================================ ================== ================== ========
|
|
Analysis GNATprove SPARK 2005 Comments
|
|
================================ ================== ================== ========
|
|
All core (SPARK) files 62% proved 06m49s 100% proved 06m07s 1
|
|
AuditLog 88% proved 00m38s 100% proved 01m46s 2
|
|
================================ ================== ================== ========
|
|
|
|
#. GNATprove was run with a timeout of 5s. The SPARK 2005 proof tools were invoked
|
|
via the command "sparksimp" with the default settings. As discussed in the body of
|
|
the report, the full conversion to SPARK 2014 is not complete so it is not possible
|
|
to make a meaningful comparison between these results. It should also be noted that
|
|
of the 2433 SPARK 2005 VCs, 100 (4%) were discharged with the aid of user-defined
|
|
proof rules and 23 (1%) were discharged by manual review. One VC is discharged by
|
|
Victor + Alt-Ergo, although this was discharged by manual review in the original
|
|
Tokeneer development (as SPARKbridge was not available at the time). If the original
|
|
manual review file is reinstated and Victor is not used then the total proof time
|
|
drops from 6m07s to 1m39s.
|
|
|
|
#. For the SPARK 2005 version of the code, the AuditLog package produces the 1 VC in
|
|
Tokeneer that is proved by Victor + Alt-Ergo. If Victor is not invoked and the
|
|
original manual review file is reinstated then the proof completes in 8 seconds.
|
|
The GNATprove results were generated with a timeout of 5s. Reducing this timeout
|
|
to 1s halves the time taken for the proof but with one fewer VC proved. It is possible
|
|
that increasing the timeout further would result in more VCs being proved at the
|
|
expense of a longer analysis time, although increasing the timeout to 300s does not
|
|
prove any additional VCs (but increases the total time to 15m47s).
|