3 ms·

The problem I’ve seen with trying to add non-static contracts to performance-sensitive languages has been ideological rather than technical. Specifically, do t

The problem I’ve seen with trying to add non-static contracts to performance-sensitive languages has been ideological rather than technical. Specifically, do the language semantics allow a mode where these checks can be turned off? Leaving them on all the time can be a huge performance burden, both directly and in the barriers they add to optimization (while there are potential optimization benefits to exploiting the guarantees of contracts, I don’t think as a practical matter they balance out). But allowing them to be turned off in “release mode” eliminates much of the benefit in all modes: Developers can no longer assume that their code always runs in a context where the contractual guarantees are met, so they have to guard data integrity or safety critical operations dynamically anyway.

touisteur 6y ago
I guess it's as bounds check and other runtime validity checks integrated in the language. When we upgrade compiler versions, I usually run a global app profile (perf, and internal tools you must have when latency and cpu load are actual product requirements. Every 'new' hot spot is analyzed and if it's a contract, I check whether there's a less costly way to perform it, or if watering down the contract seems OK (usually not). The thing is, a precondition (especially if you went through AoRTE, or silver-level SPARK) can authorize you to aggressively remove all runtime checks (and get far more performant code) 'behind'.
nerdponx 6y ago
Is it not possible to use refinement types to erase some (but maybe not all) runtime checks but still maintain a type safety guarantee?
csb6 6y ago
They can be turned off for release mode, and the SPARK subset of Ada can use them in formal verification, proving that the conditions hold true for all inputs statically, eliminating the need for any checks. I think the performance impacts are usually not as big as you think (the Ada compiler is smart enough to eliminate redundant checks where it can), and I believe that they can be turned off per package, too, so for performance critical modules they can be deactivated in release mode. I do not think contracts were intended to raise recoverable errors in a normal application's behavior; if they are triggered, then the program is incorrect, not just encountering an error. I think most developers would leave them on in release mode (if possible) just to get stack traces and exception messages to see what failed.
rramadass 6y ago
The paper "Applying Design by Contract" by Bertrand Meyer shows how DbC is to be used. It is sufficient to have only preconditions turned on by default in "release" mode, others are optional. My thumb rule is to have all preconditions/postconditions/invariants turned on only in the boundary functions (i.e. public api) of a module while the inner cohesive functions only have preconditions turned on.
OneWingedShark 6y ago
> Specifically, do the language semantics allow a mode where these checks can be turned off? Leaving them on all the time can be a huge performance burden, both directly and in the barriers they add to optimization (while there are potential optimization benefits to exploiting the guarantees of contracts, I don’t think as a practical matter they balance out). Yes, with Ada it is typically a pragma or compiler-flag to turn checks off; however, Ada has a long history of having mandatory-checks and strongly-encouraging compiler-implementers to optimize the checks away when it is known they cannot fail (which is a surprising chunk of the time if you're coming from a C-based language).

touisteur 6y ago

I guess it's as bounds check and other runtime validity checks integrated in the language. When we upgrade compiler versions, I usually run a global app profile (perf, and internal tools you must have when latency and cpu load are actual product requirements. Every 'new' hot spot is analyzed and if it's a contract, I check whether there's a less costly way to perform it, or if watering down the contract seems OK (usually not). The thing is, a precondition (especially if you went through AoRTE, or silver-level SPARK) can authorize you to aggressively remove all runtime checks (and get far more performant code) 'behind'.

nerdponx 6y ago

Is it not possible to use refinement types to erase some (but maybe not all) runtime checks but still maintain a type safety guarantee?

csb6 6y ago

They can be turned off for release mode, and the SPARK subset of Ada can use them in formal verification, proving that the conditions hold true for all inputs statically, eliminating the need for any checks. I think the performance impacts are usually not as big as you think (the Ada compiler is smart enough to eliminate redundant checks where it can), and I believe that they can be turned off per package, too, so for performance critical modules they can be deactivated in release mode. I do not think contracts were intended to raise recoverable errors in a normal application's behavior; if they are triggered, then the program is incorrect, not just encountering an error. I think most developers would leave them on in release mode (if possible) just to get stack traces and exception messages to see what failed.

rramadass 6y ago

The paper "Applying Design by Contract" by Bertrand Meyer shows how DbC is to be used. It is sufficient to have only preconditions turned on by default in "release" mode, others are optional. My thumb rule is to have all preconditions/postconditions/invariants turned on only in the boundary functions (i.e. public api) of a module while the inner cohesive functions only have preconditions turned on.

OneWingedShark 6y ago

> Specifically, do the language semantics allow a mode where these checks can be turned off? Leaving them on all the time can be a huge performance burden, both directly and in the barriers they add to optimization (while there are potential optimization benefits to exploiting the guarantees of contracts, I don’t think as a practical matter they balance out). Yes, with Ada it is typically a pragma or compiler-flag to turn checks off; however, Ada has a long history of having mandatory-checks and strongly-encouraging compiler-implementers to optimize the checks away when it is known they cannot fail (which is a surprising chunk of the time if you're coming from a C-based language).