Tutti usano librerie matematiche (cioè, libm), che forniscono approssimazioni per funzioni elementari. Sorprendentemente (o no), le librerie matematiche tradizionali (cioè le libm di Intel e GCC) non producono risultati corretti per diverse migliaia di input! Gli sviluppatori di sistemi software moderni ne sono raramente consapevoli, il che influenza la riproducibilità e la portabilità dei sistemi software. Questo post sul blog descrive il nostro nuovo metodo per sintetizzare le funzioni elementari che produce risultati corretti per tutti gli input, ma è anche significativamente più veloce dello stato dell’arte delle librerie, che sono state ottimizzate per decenni. Le funzioni elementari sono funzioni di una singola variabile che sono definite come l’esecuzione di addizione, moltiplicazione e composizione di un numero finito di polinomi, funzioni logaritmiche e funzioni trigonometriche. Il risultato di una funzione elementare è tipicamente un valore irrazionale. Quindi, ci sono due sfide principali nell’approssimazione. In primo luogo, sviluppare approssimazioni polinomiali che, quando valutate con numeri reali, minimizzano l’errore rispetto a una funzione elementare è impegnativo (cioè, c’è inevitabilmente qualche errore di approssimazione). In secondo luogo, le implementazioni software e hardware utilizzano rappresentazioni a precisione finita (ad esempio, in virgola mobile (FP)) e la valutazione di qualsiasi approssimazione polinomiale subirà un ulteriore errore di arrotondamento. È impegnativo determinare la quantità di precisione richiesta per produrre risultati corretti per tutti gli input (cioè, il dilemma del costruttore di tabelle). Anche se c’è un grande lavoro seminale sull’approssimazione delle funzioni elementari (si veda il libro di Jean-Michel Muller sulle funzioni elementari per una panoramica), gli standard raccomandano ancora risultati corretti per le funzioni elementari ma non li richiedono. L’obiettivo generale del nostro progetto RLIBM è di rendere le funzioni elementari arrotondate correttamente obbligatorie piuttosto che una raccomandazione degli standard (almeno per 32 bit o meno). Nel nostro progetto RLIBM, abbiamo fatto un caso per generare polinomi che approssimano il risultato correttamente arrotondato di f(x) piuttosto che il valore reale di f(x) perché il nostro obiettivo è quello di generare implementazioni corrette, ma efficienti. Approssimando il risultato correttamente arrotondato, consideriamo sia gli errori di approssimazione (cioè, l’approssimazione polinomiale) che gli errori di arrotondamento (cioè, con la valutazione polinomiale con rappresentazioni di precisione finita), il che permette la generazione di risultati corretti. Si possono usare librerie ad alta precisione esistenti, che sono
