Sunrise

A Verified Verification Condition Generator

Timing Results

This page describes the speed of various implementations of the Sunrise system. In particular, it reports on the time of running the automatic functions that check the well-formedness of a program and generate the verification conditions which are the remaining proof obligation.

Timing Results

The following table is the result of testing the securely verified VCG on several different example programs. The examples used here are the same ones described in chapter 8 of Homeier's dissertation. The VCG is run on several different host machines, under a variety of operating systems, versions of HOL, and versions of the Sunrise system itself. Both the examples and the host systems are briefly described after these tables.

Secure VCG execution times, in seconds
Example	Mac IIfx	Sparc 20	UltraSparc	Indigo2,6.0	Indigo2,6.1	Enterprise
quot/rem	920.1 s	176.5 s	68.2 s	13.509 s	5.528 s	3.535 s
91 function	1401.2 s	229.1 s	88.8 s	20.337 s	6.952 s	4.201 s
odd/even	4197.5 s	871.2 s	335.7 s	76.490 s	16.977 s	11.638 s
product	???	6470.6 s	2473.6 s	519.956 s	127.892 s	88.928 s
bicycling	3075.6 s	654.3 s	248.0 s	54.267 s	17.004 s	10.997 s

The following table interprets the timing results by considering the speed of the Sparc 20 system to be 1.0, and gives the speed of each system in relation to Sparc 20. This factors out the inherent difficulty of each example (approximately), and shows the relative speed of each implementation.

Secure VCG executions, times faster than Sparc 20
Example	Mac IIfx	Sparc 20	UltraSparc	Indigo2,6.0	Indigo2,6.1	Enterprise
quot/rem	0.19 x	1 x	2.6 x	13.1 x	31.9 x	49.9 x
91 function	0.16 x	1 x	2.6 x	11.3 x	33.0 x	54.5 x
odd/even	0.21 x	1 x	2.6 x	11.4 x	51.3 x	74.9 x
product	???	1 x	2.6 x	12.4 x	50.6 x	72.8 x
bicycling	0.21 x	1 x	2.6 x	12.1 x	38.5 x	59.5 x
Geometric Mean	0.19 x	1 x	2.6 x	12.0 x	40.2 x	61.5 x

The Indigo2,6.1 system is one of the fastest of those listed, so it is interesting to consider how other systems compare to it. The following table gives the relative speeds of each system on each example in terms of how many times it is slower than Indigo2,6.1.

Secure VCG executions, times slower than Indigo2,6.1
Example	Mac IIfx	Sparc 20	UltraSparc	Indigo2,6.0	Indigo2,6.1	Enterprise
quot/rem	166.4 x	31.9 x	12.3 x	2.4 x	1 x	.64 x
91 function	201.6 x	33.0 x	12.8 x	2.9 x	1 x	.60 x
odd/even	247.2 x	51.3 x	19.8 x	4.5 x	1 x	.69 x
product	???	50.6 x	19.3 x	4.1 x	1 x	.70 x
bicycling	180.9 x	38.5 x	14.6 x	3.2 x	1 x	.65 x
Geometric Mean	196.8 x	40.2 x	15.4 x	3.3 x	1 x	.65 x

Descriptions of host systems:

Mac IIfx:
Macintosh IIfx, 40 MHz 68030 CPU, 20 MB RAM, System 7.5,
HOL88 v. 2.02, on Macintosh Allegro Common Lisp (MACL),
Sunrise version 5.0.
This machine was the platform used for the creation of Sunrise v. 5.0 (and previous versions), which is the version described in the dissertation. The version of HOL used was a personal port.
(???) The attempted execution of example "product" on Mac IIfx never completed; the machine always crashed after over six hours of computation.

Sparc 20:
Sun SPARCsystem 20, 2 x 60 MHz TI,TMS390Z55 CPUs, 160 MB, SunOS 5.4,
HOL88 v. 2.02, on Austin Kyoto Common Lisp (AKCL),
Sunrise version 5.1.
This UCLA machine was the platform used for the creation of Sunrise v. 5.1, as the first UNIX version.

UltraSparc:
Sun Ultra 2 Model 1200, 200 MHz UltraSPARC CPU, 128 MB RAM, SunOS 5.5.1,
HOL88 v. 2.02, on Austin Kyoto Common Lisp (AKCL),
Sunrise version 5.1.
This was the main public UCLA machine in July 1997.

Indigo 2,6.0:
Silicon Graphics Indigo 2, IRIX 6.2, IP22,
HOL90 v. 9, on Standard ML of New Jersey, Version 109.26.1,
Sunrise version 6.0.
This version is a direct translation of Sunrise version 5.1 from HOL88 to HOL90.

Indigo 2,6.1:
Silicon Graphics Indigo 2, IRIX 6.2, IP22,
HOL90 v. 9, on Standard ML of New Jersey, Version 109.26.1,
Sunrise version 6.1.
This version is an improved version of Sunrise version 6.0, where the functions that applied the VCG to individual programs were rewritten for speed, with no sacrifice of security.

Enterprise:
Sun Enterprise 3000, 2 x 250Mhz UltraSPARC CPUs, 512MB RAM, SunOS 5.5.1,
HOL90 v. 7, on Standard ML of New Jersey, Version 0.93,
Sunrise version 6.1. The Sunrise system is almost exactly the same as for Indigo 2,6.1 above.

Descriptions of examples:

quot/rem:
Quotient/remainder program, one while loop, nonrecursive. 1 procedure, 18 lines of code. Algorithm uses repeated subtraction to compute the quotient and remainder. Generates 3 verification conditions.

91 function:
McCarthy's "91" function, using a recursive procedure. 1 procedure, 18 lines of code. Program has surprisingly simple behavior given its definition. All three verification conditions generated are solved by decision procedures.

odd/even:
Odd/even program, using two mutually recursive procedures. 2 procedures, 33 lines of code. Generates 9 verification conditions.

product:
Pandya and Joseph's program for integer multiplication, using three mutually recursive procedures. Added quotient/remainder procedure from quot/rem in order to calculate divisions. 4 procedures, 68 lines of code. Generates 13 verification conditions.

bicycling:
"Bicycling" program, using two mutually recursive procedures. Purpose is to prove termination, beyond Pandya and Joseph's method. 2 procedures, 36 lines of code. Generates 8 verification conditions.

Return to Sunrise Home Page
Return to Formal Specification in HOL Home Page