不久前，使用Microsoft Word的人會通過明確告訴該軟件運行“拼寫檢查”來檢查拼寫錯誤。這項檢查花了幾秒鐘的時間，然后用戶可以進入并解決他們的錯字。如今，我撰寫此故事時，拼寫檢查會隨著用戶的編寫自動運行。

Microsoft Word及其對Spell Check的持續(xù)運行是“并發(fā)”編程的基本示例，這是一種計算形式，其中可執(zhí)行文件與其他程序和計算同時運行。如今，大多數(shù)程序都是并發(fā)程序，從您的操作系統(tǒng)到很多應(yīng)用程序，從文字處理到Web瀏覽，人們每天都在使用它們。

CyLab的電氣與計算機工程與計算機科學(xué)系副教授Bryan Parno表示：“當您同時發(fā)生多件事情時，您需要某種協(xié)調(diào)方式，以確保彼此之間不會互相踩踏。”部門。“從歷史上看，這是一個非常麻煩的過程。”

Parno和一組研究人員最近發(fā)布了一種用于高性能并發(fā)程序的新編碼語言和工具，可確保程序可證明是正確的-即，該代碼在數(shù)學(xué)上被證明可以正確計算。在今年的編程語言設(shè)計與實現(xiàn)會議上介紹了名為Armada的語言和工具，該論文獲得了杰出論文獎。

“ Armada的新穎之處在于它的設(shè)計非常靈活，因此您可以按照自己的方式編寫代碼，從而使其能夠盡快運行，” Parno說。“但您仍將獲得有力的保證，它將做正確的事情，并且不會弄亂后端的任何事情。”

帕諾(Parno)將并發(fā)程序的復(fù)雜性及其對錯誤的敏感性比作拍賣。通常，一個拍賣師會收到很多人的出價。如此之多的人和一位拍賣師，可能需要很長時間才能達到最高出價。如果將每個人分成十個房間，每個房間都有自己的拍賣師，那將會加快速度，但拍賣師很難保持協(xié)調(diào)。會有很多錯誤的余地。

帕爾諾說：“所有拍賣商都必須有一種相互交流的方式，同時努力爭取所有房間的最高出價。” “這可能會變得非常復(fù)雜，這就是為什么您通常不會看到以這種方式進行拍賣的原因。”

帕爾諾認為，艦隊將使編寫并發(fā)程序的任何人受益，這些并發(fā)程序涵蓋了廣泛的應(yīng)用程序。

“從薪資系統(tǒng)到醫(yī)院記錄再到任何形式的電子商務(wù)，它們都由數(shù)據(jù)庫支持，而數(shù)據(jù)庫始終將由并發(fā)軟件支持，” Parno說。“除了簡單的程序，如今，幾乎所有內(nèi)容都具有某種并發(fā)性。”