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

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

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