用形式化方法構(gòu)建安全的線程機(jī)制.pdf

1、并發(fā)系統(tǒng)的安全性隨著其流行程度的增加，顯得日益重要。以往在這方面大多數(shù)研究的重點(diǎn)是，在并發(fā)機(jī)制的實(shí)現(xiàn)(OS，線程庫)已經(jīng)安全的假定下，如何保證并發(fā)程序本身的安全性。對于如何保證并發(fā)機(jī)制本身的安全性，目前的解決方案不是不完整，就是非常復(fù)雜。到了如今，大多數(shù)并發(fā)機(jī)制的實(shí)現(xiàn)者仍然主要依賴傳統(tǒng)的動態(tài)測試方法來保證代碼的安全性。 為了探索如何用形式化驗(yàn)證的方法來保證并發(fā)機(jī)制本身的安全，本文中設(shè)計(jì)了一個類似GNU pth library的用

2、戶級別線程庫，并用類MIPS的匯編語言編寫了它的一個實(shí)現(xiàn)。與通常的線程庫不同的是，該線程庫攜帶了安全規(guī)范及其證明。這些規(guī)范與證明保證，如果用戶程序?qū)υ摼€程庫API的調(diào)用始終滿足規(guī)范，那么線程庫的代碼必然可以安全執(zhí)行。更重要的是，從這些規(guī)范與證明不僅能得到線程庫本身的安全性，還能得到線程庫和用戶程序交互的安全性。為了讓本文的驗(yàn)證方法可以用于更復(fù)雜的代碼，文中還提出了一些簡化程序規(guī)范和降低證明代價(jià)的方法。 本文中的所有形式化工作，都