Una libreria conforme allo standard IEEE 1788-2015 per calcoli intervallari arrotondati correttamente

Abstract

La tesi si chiede se una libreria intervallare scritta per la velocità possa essere resa conforme allo standard IEEE 1788-2015 senza perdere ciò che la rende utile, e quanto costi la conformità. L'aritmetica intervallare calcola su insiemi di numeri reali invece che su una sola approssimazione, e il risultato contiene con certezza la risposta esatta. È la garanzia che serve a un predicato geometrico, che decide un segno invece di stimarlo. Vale dove le regole sono fissate, e le fissano due standard: IEEE 1788-2015 per gli intervalli, IEEE 754-2019 per i loro estremi. TIGHT è quella libreria: il nucleo numerico di un sistema di predicati geometrici, la cui aritmetica passa per un kernel senza rami, NFG. È stata costruita per la velocità, non per lo standard.

La conformità si ottiene quasi per intero nello strato che avvolge il kernel, ma non del tutto: esso ripara soltanto ciò che riconosce dagli operandi prima di chiamare, e un difetto del kernel sbaglia il valore su due intervalli finiti.

Settantuno modifiche atomiche chiudono i tredici blocchi di clausole della roadmap concordata con il relatore, ciascuna con clausola, commit e blocco di test. La correttezza è giudicata da un corpus esterno scritto per altre librerie, cresciuto da 4358 a 9433 asserzioni. Ventisei righe falliscono ancora, dodici perché la risposta data qui è più stretta dell'attesa e racchiude comunque il valore esatto. La copertura è stabilita leggendo uno per uno i 192 obblighi dello standard. Nove difetti del kernel rispetto a IEEE 754-2019 sono stati analizzati, e quattro correzioni sono nel repository ufficiale.

Il costo è stato misurato su un banco con margine calibrato. Sulle 332 celle in cui le due compilazioni rispondono uguale, il sovrapprezzo mediano segue il costo dell'operazione: quindici per cento sotto i due nanosecondi, due oltre i cento. La conformità si sceglie con un flag di compilazione, così il comportamento su cui i predicati poggiano sopravvive accanto a quello nuovo.

This thesis asks whether an interval library written for speed can be made conformant to the interval arithmetic standard IEEE 1788-2015 without giving up what makes it useful, and what conformance costs. Interval arithmetic computes with sets of real numbers instead of a single approximation, and its result is guaranteed to contain the exact answer. That guarantee is what a geometric predicate needs: it decides a sign rather than estimating one. It holds only where the rules are fixed, and two standards fix them: IEEE 1788-2015 for the intervals, IEEE 754-2019 for their endpoints. TIGHT is that library: the numeric core of a system of geometric predicates, whose arithmetic runs through a branch-free kernel of its own, NFG. It was built for speed, not for the standard.

Conformance can be obtained almost entirely in the wrapper above the kernel, but not entirely: the wrapper repairs only what it recognises from the operands before calling, and one kernel defect gives a wrong value on two finite intervals.

Seventy-one atomic changes close the thirteen blocks of clauses of the roadmap agreed with the supervisor, each with one clause, one commit and one test block. Correctness is decided against an external corpus written for other libraries, grown from 4358 to 9433 assertions. Twenty-six lines still fail, twelve because the answer given here is tighter than the corpus expects and still encloses the exact result. Coverage is established by reading the standard's 192 obligations one at a time. Nine kernel defects against IEEE 754-2019 were analysed, and four repairs are in its official repository.

The cost was measured on a benchmark with a calibrated margin. Over the 332 cells in which both builds answer the same, the median surcharge follows the cost of the operation: fifteen per cent on those below two nanoseconds, two per cent on those above a hundred. Conformance is selected by a compilation flag, so the behaviour the predicates rely on survives beside it.