★北京廣利核系統工程有限公司程建明，徐先柱

關(guān)鍵詞：嵌入式操作系統；數學(xué)庫函數；對比測試；誤差分析

核鷺操作系統（NuEgretOS）是北京廣利核系統工程有限公司開(kāi)發(fā)的嵌入式多任務(wù)操作系統軟件，可運行于基于龍芯2K1000處理器的專(zhuān)用硬件環(huán)境中，為執行核安全重要功能的、符合包含IEC 62138-2018^[1]等標準要求的應用軟件提供操作系統軟件環(huán)境。NuEgretOS提供在目標硬件環(huán)境下資源分配、調度、輸入輸出控制以及數據管理等服務(wù)，應用軟件在此基礎上提供信號和控制處理邏輯。NuEgretOS還提供部分C語(yǔ)言標準庫函數（其中包含數學(xué)庫函數），供基于NuEgretOS運行的應用軟件設計時(shí)調用。其中，NuEgretOS數學(xué)庫目前提供最常用的若干數學(xué)函數，包括三角函數、反三角函數、雙曲函數、指數和對數函數、冪函數，以及與浮點(diǎn)數特性相關(guān)的函數（如取整、取余、取絕對值、切分浮點(diǎn)數）等。

出于安全方面的原因，NuEgretOS數學(xué)庫實(shí)現過(guò)程中不使用任何第三方函數庫，包括不調用編譯器自帶的數學(xué)函數庫中的函數。同時(shí)，由于NuEgretOS數學(xué)庫函數將直接參與應用軟件處理邏輯，執行包括核安全重要功能在內的應用軟件功能，因此在使用前必須對其進(jìn)行全面驗證和確認。通過(guò)測試保證其正確性和計算精度是NuEgretOS數學(xué)庫驗證和確認的重要工作之一。

1　庫函數設計NuEgretOS軟件和應用軟件均使用C語(yǔ)言及必要的

匯編語(yǔ)言開(kāi)發(fā)，使用GCC工具進(jìn)行編譯。NuEgretOS以鏡像文件（.bin文件）方式存儲于目標硬件中的存儲器上，并在設備上電時(shí)加載運行。NuEgretOS的C語(yǔ)言標準庫（其中包含數學(xué)庫函數）以庫文件（.a文件）的形式提供給應用開(kāi)發(fā)環(huán)境，并與應用軟件代碼一起編譯生成可執行與可鏈接格式文件（elf格式，.out文件），由NuEgretOS加載和運行。

NuEgretOS數學(xué)庫（C語(yǔ)言標準庫的一部分）中的全部函數定義和POSIX.1-2017^[2]標準中對應的函數相同，是POSIX.1-2017規定的數學(xué)函數的子集。

NuEgretOS數學(xué)庫各函數輸入和輸出中的數學(xué)上定義為實(shí)數的數值均使用double類(lèi)型浮點(diǎn)數表示，該浮點(diǎn)數類(lèi)型符合ISO/IEC 60559：2020（IEEE Std754-2019）^[3]對64位雙精度浮點(diǎn)數（binary64）的規定。double型數據位串定義如圖1所示。

圖1 double型數據位串定義

按該標準定義，double型數以64位位串值（二進(jìn)制內存值）表示實(shí)數域內的若干個(gè)（264-253-1，約1.84×1019個(gè)）離散數值（有限小數，含整數）以及計算機在處理小數運算時(shí)的特殊定義值（不表示任何實(shí)數的位串值，僅用于計算機對浮點(diǎn)數處理的特殊情況的表示）。double型數據位串值定義細分類(lèi)別及特點(diǎn)如表1所示。

表1 double型數據位串值定義細分類(lèi)別及特點(diǎn)

2　測試設計

2.1　計算誤差來(lái)源分析

基于ISO/IEC60559：2020（IEEE Std754-2019）^[3]對64位雙精度浮點(diǎn)數（binary64）的規定，雙精度浮點(diǎn)數除特殊定義值外，兩個(gè)位串值相鄰的浮點(diǎn)數數值之間的差值的絕對值定義為1個(gè)ULP（unit in the last place，最小有效數）。1ULP的實(shí)際表示值與指數域的大小相關(guān)：當指數域為最大值0x7FE時(shí)，1ULP≈8.99E307；當指數域為最小值0x000時(shí)，1ULP≈4.94E-324。對于浮點(diǎn)數表示范圍（約-1.79E308~約1.79E308）內的任意實(shí)數，在最近舍入模式下，由浮點(diǎn)數離散特性帶來(lái)的最大表示誤差≤0.5ULPs。規格化數的二進(jìn)制有效數字個(gè)數為53個(gè)，由浮點(diǎn)數舍入帶來(lái)的最大表示誤差（≤0.5ULPs）帶來(lái)的數值相對誤差范圍為（2-54，2-53），非規格化數的二進(jìn)制有效數字個(gè)數最大為52個(gè)，隨數值減小而減少，由浮點(diǎn)數舍入帶來(lái)的最大表示誤差（≤0.5ULPs）造成的數值相對誤差也相應增大，范圍為（2-53，2-1）。

對于NuEgretOS數學(xué)庫中與浮點(diǎn)數特性相關(guān)的算術(shù)函數（如取整、取余、取絕對值、切分浮點(diǎn)數等），函數的運算輸出與其理論輸出之間不應存在誤差，即允許誤差為0ULPs。而對于其它函數，包括三角函數、反三角函數、雙曲函數、指數和對數函數、冪函數等，其理論計算值與其函數輸出值之間的誤差受多種因素影響，主要包括：

（1）輸入值表示誤差；

（2）計算方法誤差，如使用泰勒展開(kāi)式有限項帶來(lái)的誤差；

（3）計算過(guò)程誤差，包括模型參數引入的誤差、中間計算結果的舍入誤差等；

（4）輸出值表示誤差?；贜uEgretOS數學(xué)庫函數的目標應用，除算術(shù)計算函數外，設定各函數輸出的允許誤差為2ULPs。

2.2　驗證目標

基于NuEgretOS數學(xué)庫的設計特點(diǎn)和應用要求，NuEgretOS數學(xué)庫的驗證目標包括：

（1）各函數在其定義域內的任意值（包括浮點(diǎn)定義的正負零值）的計算輸出值正確（符合函數定義）且在允許誤差范圍內。

（2）各函數對異常及特殊情況處理正確，包括對計算值超浮點(diǎn)表示范圍的處理、輸入非函數定義域數值、輸入浮點(diǎn)特殊定義值等，函數輸出符合處理器特性以及IEC60559規定的特殊定義值。如有定義，NuEgretOS應用軟件可通過(guò)注冊中斷處理程序獲知計算過(guò)程例外或異常并處理。

2.3　測試方案

NuEgretOS數學(xué)庫為新開(kāi)發(fā)軟件，各函數遵循其數學(xué)定義，其輸出值實(shí)數范圍內存在理論精確值，該理論精確值在確定的浮點(diǎn)數類(lèi)型定義和舍入方式下，經(jīng)計算機計算后輸出的浮點(diǎn)數（二進(jìn)制內存值）是唯一的和確定的，與函數的實(shí)現方式以及運行所依賴(lài)的硬件和軟件環(huán)境無(wú)關(guān)。同時(shí)，NuEgretOS數學(xué)庫范圍內的各函數已在支持POSIX標準的大多數軟件開(kāi)發(fā)工具及編譯工具中實(shí)現。這些已實(shí)現的函數多包含在隨軟件開(kāi)發(fā)工具及編譯工具提供的函數庫中，其實(shí)現比較成熟且已有較多運行經(jīng)歷，運算結果相對可信，NuEgretOS數學(xué)庫測試時(shí)假定對應函數的預期運算結果。當運算結果一致時(shí)，可在較高可信度上證明NuEgretOS數學(xué)庫函數的正確性和精度，當運算結果不一致時(shí)，進(jìn)行函數實(shí)現分析以定位問(wèn)題或通過(guò)設計分析證明NuEgretOS數學(xué)庫函數的正確性和精度。測試前對NuEgretOS數學(xué)庫全部函數的設計和實(shí)現代碼的評審和分析也是保證NuEgretOS數學(xué)庫函數的正確性和精度的措施。因此，可以通過(guò)對比其它已實(shí)現的成熟函數庫執行結果的方式，對NuEgretOS數學(xué)庫的正確性和精度進(jìn)行對比測試。NuEgretOS數學(xué)庫對比測試總體方案如圖2所示。

圖2 對比測試方案

分別建立數學(xué)庫的參考運行環(huán)境和目標機運行環(huán)境，目標機運行環(huán)境和NuEgretOS應用軟件運行環(huán)境完全一致。在參考運行環(huán)境下，可以用與NuEgretOS應用程序相同的方式調用相同定義的各數學(xué)庫函數。參考運行環(huán)境由通用PC機搭建，同時(shí)作為測試應用程序的開(kāi)發(fā)環(huán)境。

用相同的方式分別建立參考環(huán)境測試工程和目標機測試工程，兩個(gè)測試工程共用一套C語(yǔ)言代碼，兩個(gè)工程中的測試應用程序內必要的有差別的行為通過(guò)預編譯開(kāi)關(guān)實(shí)現。測試應用程序中含用例生成、用例執行、結果保存、用例讀取、結果比較等主要功能模塊。參考環(huán)境應用程序實(shí)際執行用例生成、用例執行、結果保存三項功能。參考環(huán)境測試應用程序運行結果保存中包括了測試用例中各函數的輸入序列和其在參考環(huán)境中的運算結果。各函數的輸入序列和對應的參考環(huán)境運算結果組成測試向量，以二進(jìn)制內存拷貝的方式保存成文件，并下載到目標機運行環(huán)境。目標機測試應用程序讀取各待測函數測試向量生成測試用例。目標機測試應用程序執行完成測試用例后進(jìn)行結果比較，以文件和串口打印輸出的形式輸出與參考環(huán)境計算結果的比較情況。同時(shí)目標機測試應用程序用與參考環(huán)境測試應用程序相同的方式保存測試結果。參考環(huán)境和目標機處理器大小端模式相同，測試向量的保存、傳遞和讀取過(guò)程不引入浮點(diǎn)數表示誤差。參考環(huán)境和目標機的測試應用程序的全部輸出作為人工分析的輸入，用以最終判定NuEgretOS數學(xué)庫的正確性和計算精度是否符合設計和應用目標。

另外，還使用不同的編譯工具生成多個(gè)參考環(huán)境測試應用程序并對其運算結果進(jìn)行比較，用以提高參考環(huán)境測試應用程序運算結果作為NuEgretOS數學(xué)庫預期結果的可信度。

2.4　測試用例生成

在本項測試中，各函數的測試輸入覆蓋率是保證對NuEgretOS數學(xué)庫各函數測試全面性的最重要指標。由于double型數據位串值個(gè)數（264）遠大于目標機運行環(huán)境可執行測試輸入數量，進(jìn)行位串值完全窮舉是不可行的，需按適當的規則進(jìn)行抽樣。

為保證充分的輸入覆蓋率，測試用例設計前先分析各函數的基本特性，包括定義域、周期（如有）、單調性、與函數計算機實(shí)現方法相關(guān)的特殊值等，再根據各函數特性和浮點(diǎn)數定義自動(dòng)生成測試輸入序列。在參考環(huán)境測試應用程序中生成各函數測試輸入值序列時(shí)，需滿(mǎn)足以下規則：

2.4.1　插入函數整體定義域邊界值、典型周期定義域邊界值、函數拐點(diǎn)值，無(wú)論函數在這些值上是否有定義；

2.4.2　插入函數整體定義域、典型周期定義域內若干（40個(gè)以上）隨機值；

2.4.3　插入與各函數實(shí)現相關(guān)的特殊值，可能包括：

（1）與函數計算方法相關(guān)的函數定義域邊界值，如sin函數中泰勒展開(kāi)式計算前x的邊界值π/4；

（2）與函數計算所用參數相關(guān)的特殊值等；

（3）函數計算過(guò)程中可能出現溢出例外的函數定義域值。

2.4.4　插入與浮點(diǎn)數定義相關(guān)的特殊值（無(wú)論數學(xué)函數在這些值上是否有定義），包括正負零、正負無(wú)窮大、qNaN（靜默非數）/sNaN（信號非數）典型值、規格化數和非規格化數的最大值和最小值。

除自動(dòng)生成的隨機數值外，以上各項中的輸入值均以C語(yǔ)言共用體方式直接對內存賦值，以避免因常量編譯等因素造成實(shí)際輸入值與需輸入值不一致。另外，在按以上規則插入各函數測試輸入值時(shí)，同時(shí)插入每個(gè)輸入值的二進(jìn)制位串值的相鄰值。

3　測試工程的編譯和運行

在參考環(huán)境中，使用MinGW提供的GCC編譯工具編譯測試工程，編譯過(guò)程中數學(xué)函數調用GCC編譯工具自帶函數庫（libgcc.a）中的對應函數實(shí)現，編譯后的測試應用程序在Windows操作系統下運行。

目標機測試工程在Windows操作系統下調用GCC編譯工具進(jìn)行交叉編譯，編譯過(guò)程中數學(xué)函數調用NuEgretOS數學(xué)庫（libEgretLibc.a）中的對應函數實(shí)現。另外，在參考環(huán)境中還調用了MSVC編譯器編譯測試工程，編譯過(guò)程中數學(xué)函數調用MSVC編譯工具自帶的C運行時(shí)庫中的對應函數實(shí)現。

4　運行結果比較

4.1　參考環(huán)境下不同編譯的測試應用程序運算結果比較

Windows操作系統下使用MinGW和MSVC編譯的測試應用程序可以相互傳遞各自生成的二進(jìn)制測試向量文件。在相同的函數輸入下，兩個(gè)程序的函數運行結果僅存在細微差別，包括：

（1）部分函數在特殊輸入值下計算值僅相差1ULP（如sqrt函數輸入最大規格化數，sin/cos函數的部分輸入值）。

（2）部分函數在輸入為NaN時(shí)，輸出的NaN位串值不同（如fabs函數是否將NaN位串值的符號位設置為0，exp函數輸出NaN時(shí)是否將位串值尾數域的全部非首位設置為0），對NaN的不同處理均不違反C99^[4]和POSIX.1-2017標準的要求。

結合MinGW和MSVC編譯工具（包括工具自帶的函數庫）的應用廣泛程度和函數輸出比較結果，以MinGW編譯工具生成的參考環(huán)境測試應用程序的運算結果作為NuEgretOS數學(xué)庫各函數的參考值是相對可信的。

4.2　參考環(huán)境和目標機運行環(huán)境測試應用程序運算結果比較

以MinGW作為參考環(huán)境測試應用程序編譯工具，并以該參考環(huán)境測試應用程序生成的各函數輸入序列作為目標機測試應用程序的被測函數輸入序列，假定該參考環(huán)境測試應用程序對自身生成的測試輸入序列的函數運算結果為目標機測試應用程序執行NuEgretOS數學(xué)庫各函數的預期結果（即參考值）。經(jīng)目標機測試應用程序運行結果比較，除以下兩項主要問(wèn)題外，NuEgretOS數學(xué)庫運算結果符合驗證目標：函數對有定義輸入值、異常及特殊情況處理正確，并且函數輸出為有限小數值的計算誤差≤2ULPs。

（1）問(wèn)題1：exp、sinh、sqrt、log、log10這5個(gè)函數輸入為非規格化浮點(diǎn)數時(shí)，計算值錯誤。部分測試結果如表2所示。

表2 問(wèn)題1測試結果

（2）問(wèn)題2：cos、sin、tan這三個(gè)周期性函數在輸入值較大時(shí)，計算誤差超允許值（2ULPs）。部分測試結果如表3所示。

表3 問(wèn)題2測試結果

5　問(wèn)題分析和處理

經(jīng)過(guò)對已發(fā)現的兩個(gè)問(wèn)題（如表2和表3所示）相關(guān)的軟件代碼進(jìn)行分析和調試，兩個(gè)問(wèn)題的原因和處理方式如下：

（1）問(wèn)題1，屬例外處理的匯編代碼錯誤。錯誤原因為匯編代碼中寄存器使用錯誤，使得NuEgretOS在處理龍芯2K1000浮點(diǎn)協(xié)處理器（FPU）的例外（未實(shí)現操作例外，2K1000未實(shí)現的MIPS64全部浮點(diǎn)指令）時(shí)的處理邏輯出現錯誤。匯編代碼修改后問(wèn)題得到解決。經(jīng)回歸測試，這5個(gè)函數（exp、sinh、sqrt、log、log10）在參考環(huán)境和目標環(huán)境的計算誤差不超過(guò)2UPLs，符合NuEgretOS數學(xué)庫預先設定的要求。

（2）問(wèn)題2，由計算參數表示誤差而引起的中間計算值誤差隨三角函數2π周期數擴大。NuEgretOS數學(xué)庫在實(shí)現cos、sin、tan這三個(gè)周期性函數，其中sin和cos函數采用這兩個(gè)函數的泰勒展開(kāi)式求解，tan函數利用tanx=sinx/cosx關(guān)系式求解。在代入泰勒展開(kāi)式前，將輸入值x通過(guò)三角函數變換公式整理到絕對值不大于π/4的弧度值。首先需利用公式（如sinx=sin(k·2π+θ),x∈R,k∈N,θ∈[-π,π]）將NuEgretOS數學(xué)庫中的三角函數定義域轉化到±π之間時(shí)，使用位串值為0x401921FB54442D18的參數（名為PI2）表示理論數值2π，其表示值（6.283185307179586231996）與精確值（6.283185307179586476925）之間的表示誤差為δPI2≈2.449×10-16，約0.276ULPs。經(jīng)過(guò)k個(gè)2π周期后，造成θ值的誤差為δθ=k·δPI2，因此|k|≥1時(shí)，這一單一因素將可以造成函數值誤差大于2ULPs。解決這一問(wèn)題可以有兩個(gè)途徑：

（1）限制函數輸入值的范圍，以減少中間值θ的計算誤差；

（2）使用更高精度的浮點(diǎn)數（如binary128或兩個(gè)binary64）表示2π的值并參與計算。

6　總結

研究者引入對比測試方法快速準確地實(shí)現了對新開(kāi)發(fā)的嵌入式操作系統數學(xué)庫的測試，并通過(guò)誤差分析輔助完成了對測試中發(fā)現的被測函數問(wèn)題的定位和處理，提高了被測試函數庫的計算精度和結果可信度。

按照經(jīng)分析確定的規則生成各被測試函數輸入值序列保證了測試的有效覆蓋率。

在參考環(huán)境中采用不同編譯工具并調用不同工具自帶函數庫執行相同輸入序列的函數計算，并對計算結果進(jìn)行比較，提高了參考環(huán)境生成的、擬作為目標機環(huán)境被測函數預期值的函數值的正確性和精度的可信度。

使用浮點(diǎn)數內存值二進(jìn)制方式保存、傳遞和比較各函數的輸入序列和對應的參考環(huán)境運算結果組成的測試向量，避免了浮點(diǎn)數值在不同環(huán)境中交換和比較可能帶來(lái)的表示誤差和比較不確定性。

通過(guò)參考環(huán)境和目標環(huán)境測試應用程序，測試用例按規則自動(dòng)生成、執行并比較結果，提高了本項測試的自動(dòng)化程度。

作者簡(jiǎn)介：

程建明（1976-），男，四川人，高級工程師，學(xué)士，現就職于北京廣利核系統工程有限公司，主要從事核安全級軟件的驗證和確認工作。

徐先柱（1982-），男，黑龍江人，高級工程師，學(xué)士，現就職于北京廣利核系統工程有限公司，主要從事于核安全級軟件的驗證與確認工作。

參考文獻：

[1] IEC 62138-2018, Nuclear power plants-Instrumentation and control systems important to safety-Software aspects for computer-based systems performing category B or C functions[S]. International Electrotechnical Commission，2018.

[2] POSIX.1-2017/IEEE Std 1003.1-2017，IEEE Standard for Information Technology-Portable Operating System Interface (POSIX?) [S]. IEEE Computer Society and The Open Group, 2017.

[3] ISO/IEC 60559:2020(E) IEEE Std 754-2019, Floating-point arithmetic[S]. 2020.

[4] ISO/IEC 9899:1999 Programming languages-C[S]. 1999.

摘自《自動(dòng)化博覽》2023年11月刊