NASA的10條代碼編寫原則及原因分析
美國(guó)宇航局(NaTIonal AeronauTIcs and Space AdministraTIon,縮寫為 NASA)是美國(guó)聯(lián)邦政府的一個(gè)獨(dú)立機(jī)構(gòu),負(fù)責(zé)制定、實(shí)施美國(guó)的民用太空計(jì)劃、與開(kāi)展航空科學(xué)暨太空科學(xué)的研究。在太空計(jì)劃之外,美國(guó)國(guó)家航空航天局還進(jìn)行長(zhǎng)期的民用以及軍用航空航天研究。
在普通人的眼中,NASA是一個(gè)很“高級(jí)”的機(jī)構(gòu),其成員包含大量不同領(lǐng)域的科學(xué)家和研究人員。與其他任何組織機(jī)構(gòu)類似,NASA的日常工作,以及所執(zhí)行的幾乎全部項(xiàng)目也離不開(kāi)計(jì)算機(jī)的輔助,出于需求的特殊性和重要性,他們所使用的很多計(jì)算機(jī)軟件都是內(nèi)部自行開(kāi)發(fā)的,在一些重要項(xiàng)目的關(guān)鍵領(lǐng)域發(fā)揮著作用。
去年,一位前NASA實(shí)習(xí)生把美國(guó)阿波羅登月項(xiàng)目的11號(hào)計(jì)算機(jī) --- 阿波羅導(dǎo)航計(jì)算機(jī) (Apollo Guidance Computer) 系統(tǒng)源代碼上傳到了 GitHub,此舉在開(kāi)發(fā)者群體中引起了極大的熱議。
此外,NASA官方也已將自己的部分源代碼開(kāi)源到 GitHub,讓我們得以管窺這一頂尖科研機(jī)構(gòu)內(nèi)的聰明大腦們寫代碼的專業(yè)水平。
大型的復(fù)雜軟件項(xiàng)目通常會(huì)遵循一定的代碼編寫標(biāo)準(zhǔn)和指南。這些指南奠定了軟件開(kāi)發(fā)過(guò)程中必須遵守的基本原則。
a) 代碼的結(jié)構(gòu)如何安排?
b) 應(yīng)當(dāng)或不應(yīng)當(dāng)使用哪些語(yǔ)言特性?
出于效果的角度考慮,這些原則必須盡可能精簡(jiǎn)并且必須足夠具體,這樣才能更好地被人理解并記憶。
本文將介紹由 NASA 噴氣推進(jìn)實(shí)驗(yàn)室首席科學(xué)家 Gerard J. Holzmann 所提出的,側(cè)重于安全參數(shù)的10條代碼編寫原則。當(dāng)然,這些原則也適用于其他編程語(yǔ)言。
為 NASA 工作的全球頂尖程序員在編寫高度安全的代碼時(shí)就沿襲了這樣的一套指南。實(shí)際上,很多組織,包括NASA噴氣推進(jìn)實(shí)驗(yàn)室主要會(huì)選擇使用C語(yǔ)言編寫代碼。
原因在于這種語(yǔ)言具備完善的工具支持,包括邏輯模型分離器、調(diào)試器、靜態(tài)編譯器、強(qiáng)源(Strong source)代碼分析器,以及度量工具等。
有時(shí)候,編寫代碼必須遵守一定的原則,尤其是在代碼的正確性會(huì)對(duì)人的生命產(chǎn)生決定性影響的領(lǐng)域,例如飛機(jī)、將宇航員送上同步軌道的航天器,以及距離居住地僅幾英里遠(yuǎn)的核電站等設(shè)施運(yùn)行的控制代碼。
原則1 – 簡(jiǎn)化控制流程(Simple Control Flow)
使用盡可能精簡(jiǎn)的控制流程構(gòu)造編寫程序 —— 不要使用setjmp或longjmp構(gòu)造、goto語(yǔ)句,以及直接或間接的recursion。
原因:簡(jiǎn)化控制流程有助于提高代碼清晰度,增強(qiáng)代碼可驗(yàn)證能力。不使用遞歸,便不會(huì)產(chǎn)生循環(huán)的函數(shù)調(diào)用圖,這樣也可證明所有本應(yīng)有界的執(zhí)行實(shí)際上都是有界的。
原則2 – 為循環(huán)使用固定次數(shù)上限(Fixed Upper Bound for Loops)
所有循環(huán)必須有固定次數(shù)的上限。我們可以通過(guò)驗(yàn)證工具靜態(tài)地證明,為循環(huán)中迭代數(shù)量所設(shè)立的上限次數(shù)未被超越。
如果無(wú)法以靜態(tài)方式對(duì)循環(huán)的次數(shù)界限加以證明,則可認(rèn)為未遵守該原則。
原因:為循環(huán)設(shè)置次數(shù)界限,避免使用遞歸,這些做法有助于預(yù)防代碼失控。然而該原則無(wú)法適用于本就不應(yīng)終止的迭代(例如進(jìn)程調(diào)度器)。此時(shí)將沿用該原則的逆向原則:必須能夠靜態(tài)地證明迭代不能終止。
原則3 – 不使用動(dòng)態(tài)內(nèi)存分配(No Dynamic Memory AllocaTIon)
不要在初始化完成后進(jìn)行動(dòng)態(tài)內(nèi)存分配。
原因:諸如malloc等內(nèi)存分配機(jī)制,以及垃圾回收器通常會(huì)產(chǎn)生無(wú)法預(yù)知的行為,進(jìn)而可能會(huì)對(duì)性能產(chǎn)生影響。更重要的是,還有可能因?yàn)槌绦騿T的失誤造成內(nèi)存錯(cuò)誤,例如:
試圖分配超過(guò)可用物理內(nèi)存數(shù)的內(nèi)存
忘記釋放內(nèi)存
繼續(xù)使用已被釋放的內(nèi)存
對(duì)已分配內(nèi)存進(jìn)行越界使用
應(yīng)強(qiáng)制所有模塊位于固定大小、預(yù)先分配的存儲(chǔ)區(qū)域中,借此可避免此類問(wèn)題,并簡(jiǎn)化內(nèi)存使用情況的驗(yàn)證工作。
堆中未分配內(nèi)存的情況下,動(dòng)態(tài)請(qǐng)求內(nèi)存的唯一方式是使用棧內(nèi)存。
原則4 – 不使用冗長(zhǎng)的函數(shù)(No Large Functions)
任何函數(shù)的長(zhǎng)度不應(yīng)超過(guò)使用標(biāo)準(zhǔn)參考格式(每個(gè)聲明最多一行,每個(gè)語(yǔ)句最多一行)打印的紙張上一頁(yè)紙所能容納的字符數(shù)。這意味著函數(shù)的代碼不應(yīng)超過(guò)60行。
原因:過(guò)長(zhǎng)的函數(shù)通常意味著結(jié)構(gòu)并非最優(yōu)。每個(gè)函數(shù)都應(yīng)是可理解且可驗(yàn)證的單一邏輯單位。如果在計(jì)算機(jī)顯示器上需要多屏界面才能完整顯示,這樣的邏輯單位通常會(huì)極難理解。
原則5 – 低斷言密度(Low Assertion Density)