Verifying Compilers
for Financial Applications
David Crocker
Escher Technologies Ltd.
Why financial applications?



Lots of money at stake if the software delivers incorrect
results
FSA sets tough audit regulations backed up by very large
fines
Business-critical software development is mostly not
outsourced to low-cost countries
03/10/2015
Verifying Compilers for Financial Applications
2
Characteristics of
investment banking software

Often very complex


Agile techniques required


Need to value handle new exotics quickly
Lots of floating-point maths


Many hundreds of classes
Used to represent money and often time
Multi-threading is increasingly important

03/10/2015
To make the best use of processor resources
Verifying Compilers for Financial Applications
3
Techniques and languages
typically used



Component-based object-oriented development

Helps to manage the complexity

Provides agility
Object-oriented programming languages

Mainly C++ and C#

Some Java, little or no UML
Often integrated with Excel spreadsheets
03/10/2015
Verifying Compilers for Financial Applications
4
What sorts of verifying compiler
might an investment bank use?

Verifying compilers for C++ and C#


Verifying compilers for annotated C++ and C#


Much too difficult in practice
e.g. MS Research “Spec #” project
Verifying compilers for specifications

03/10/2015
e.g. Perfect Developer
Verifying Compilers for Financial Applications
5
Verification with annotated
programming languages
Examples: ESC/Java, SPARK, Spec #
Advantages:



Disadvantages:
Based on a standard programming
language
Easier to introduce into a
development process
Can use on existing code by
adding the annotations
03/10/2015


Java, C# etc. were not designed for
verification
Correctness and completeness must
be sacrificed, or the language must
be severely subsetted

Large volume of annotation needed

Loops and aliasing are big problems

Hard to express data refinement
Verifying Compilers for Financial Applications
6
The problem with loops




Consider a method that contains a loop
To verify code that follows the loop, we need to know the
state of the system just after the loop
This means we need to know the loop invariant
Loop invariants are often very difficult to determine even
for experts!
03/10/2015
Verifying Compilers for Financial Applications
7
The problem with aliasing



Changing the value of one variable also changes the
values of other variables it is aliased to
Most O-O languages use reference semantics by default
Inheritance, polymorphism and dynamic binding greatly
increase the possibility of aliasing

03/10/2015
The number of anti-aliasing annotations potentially needed
becomes HUGE!
Verifying Compilers for Financial Applications
8
Why are we still using
people to write programs?

Our view: Traditional programming is obsolete!



C, Ada, C# etc. should play the same role today that assembly
languages did 20 years ago
Most code should be generated from specifications
Manual refinement is sometimes needed


03/10/2015
Where a more efficient data representation is needed
Where code generated directly from specifications is [currently]
not efficient enough
Verifying Compilers for Financial Applications
9
Specify-Refine-Generate approach
Examples: B-method, Perfect Developer



Specify the system at multiple levels

Behavioural and state-based specifications

Verify the specifications for consistency and “completeness”
Refine the specifications

Manually (within the same notation) and automatically

Verify that the refinements are correct
Generate code in a standard programming language

03/10/2015
C++, Java, C#, Ada…
Verifying Compilers for Financial Applications
10
Advantages


The notation is designed for verification

e.g. value semantics by default, polymorphism only on demand

Automated verification is much more tractable
The user is largely spared from writing loop invariants


92% of all loops are generated from specifications
The user is encouraged to write the specification first

03/10/2015
The most expensive errors are detected earlier
Verifying Compilers for Financial Applications
11
Adapting Perfect Developer
for investment banking

Floating point model had to be relaxed


Multiple inheritance of interfaces was added


e.g. we now assume (a + b) + c = a + (b + c) for type real
Component-based systems are typically built around interfaces
C# code generation will be needed

03/10/2015
Currently we generate C++ (subset), Java, partial Ada
Verifying Compilers for Financial Applications
12
Example: valuing European options

Vanilla European call and put options can be valued using
the Black-Scholes formula


There is an expected relation between the values of a
call option and the corresponding put option


Based on stochastic calculus
A “no arbitrage” agreement predicts “call-put parity”
We wish to verify:


03/10/2015
For any input that obeys the declared preconditions, the valuator
shall not crash
The valuator obeys call-put parity
Verifying Compilers for Financial Applications
13
03/10/2015
Verifying Compilers for Financial Applications
14
First attempt at verification
03/10/2015
Verifying Compilers for Financial Applications
15
“Unproven” output file
03/10/2015
Verifying Compilers for Financial Applications
16
Correcting the Specification
function putValue(today: Date, assetPrice: Money, rate: real, vol: Volatility)
: Money
pre today <= maturity,
Insufficient
assetPrice > 0.0
precondition
^= ( let ttm ^= maturity - today;
let vSqrtT ^= vol * sqrt(ttm);
let d1 ^= (log(assetPrice/strike) + (rate + vol*vol/2.0) * ttm)/vSqrtT;
let d2 ^= d1 - vSqrtT;
strike * exp(-rate * ttm) * cunorm(-d2) + assetPrice * cunorm(-d1)
);
Incorrect sign
03/10/2015
Verifying Compilers for Financial Applications
17
Verifying the corrected specification
03/10/2015
Verifying Compilers for Financial Applications
18
Extract from the generated proofs
03/10/2015
Verifying Compilers for Financial Applications
19
Does Perfect Developer meet the
challenges of financial software?


Complexity

Complexity is less than PD itself, so not a problem

We now have a 64-bit version of PD to handle larger proofs
Floating point maths


03/10/2015
Using the relaxed FP model we can prove some useful properties
We cannot guarantee absence of overflow/underflow or the
accuracy of the result
Verifying Compilers for Financial Applications
20
What about multi-threading?

Processor clock speeds have reached a plateau


Processor development is now centred on multiple cores


But transistor counts are still increasing
Future applications must be multithreaded to take advantage of
increasing processor power
We need to handle two sorts of concurrency:
03/10/2015

Distributed systems (use CSP + model checking)

Thread-level concurrency with shared variables
Verifying Compilers for Financial Applications
21
How should we handle
thread-level concurrency?


The traditional approach is to use locks

Implemented in some languages as synchronised methods/objects

But programmers frequently use them incorrectly
The compiler should manage access to shared variables


But automating the creation and use of locks is not very
satisfactory because…
Locks do not compose

03/10/2015
If we compose components that use locks, we can get deadlock,
priority inversion and other problems
Verifying Compilers for Financial Applications
22
Transactional Memory to the rescue!

Relieves the programmer from having to worry so much
about access to shared variables



Avoids deadlock and priority inversion
Can be implemented in software

STM has been implemented for a Java compiler

Even better, implement it in the Java or .NET runtime
See (e.g.) the paper by Simon Peyton-Jones et al for
more details

03/10/2015
http://research.microsoft.com/Users/simonpj/papers/stm/stm.pdf
Verifying Compilers for Financial Applications
23
Further work needed

Formalising practical floating point maths


Concurrency


Do CSP and TM between them cover all our needs?
Reaching 100% automated verification most of the time


In conjunction with experts in numerical algorithms
Inductive proofs are occasionally needed
Handling proof failures

03/10/2015
Provide even better suggestions to the user
Verifying Compilers for Financial Applications
24
Conclusion

Verifying compilers for specifications of complex
single-threaded applications already exist


Extending this to cover shared-memory multi-threaded
applications should be possible within 5 years


95% to 100% automated proof is currently achieved
Provided that transactional memory lives up to expectations
More research is needed before we can fully verify
systems using floating point arithmetic
03/10/2015
Verifying Compilers for Financial Applications
25
“Software inevitably contains bugs”
- let’s dispel that myth!
Appendix: What others think of Perfect Developer
“PD is the only tool of the four that comes close to the ideal of automatic
and easy program verification.”
Ingo Feinerer, MSc thesis, Technischen Universität Wien
“In comparison with other tools, PD offers a software oriented approach
to refinement rather than a brutally mathematical one …
… PD supports specification and implementation in a relatively simple
language, so its learning curve is quite gentle for practicing software
engineers.”
Gareth Carter, Software Engineering and Formal Methods 2005
03/10/2015
Verifying Compilers for Financial Applications
27
Appendix: Some application statistics
Compiler/
verifier
Terminal
emulator
Government
IT pilot
114720
3192
13777
229367
6752
38858
Verification conditions
131441
1349
2645
% valid proved
> 96%
 98.6%
 99.7%
Seconds per condition
4.5
2.4
3.7
Perfect source lines
1
Generated C++ lines
1
Including comments
03/10/2015
2
2
No comments; runtime checks not generated
Verifying Compilers for Financial Applications
28
Descargar

Turning Functional Specifications into Verified Code