电脑当掉资料也不会遗失的档案系统
三名来自麻省理工学院（MIT）电子工程系（EECS）的研究职员利用形式验证（formal verification）的程序建立了一个纵然电脑忽然当掉也不会造成资料遗失的档案系统，相干研究成果并准备在今年10月举行的作业系统学术会议ACM Symposium on Operating Systems Principles（SOSP）上发表。
MIT电子工程系副传授Nickolai Zeldovich表示，很多人都担心档案系统的稳定性，岂论是在正常运作的状况下，或是在电脑当机、电源妨碍、硬体妨碍，或是软体呈现臭虫的时候，而且利用者还会发现，就算是颠末严谨测试的档案系统，其当机回复复兴功能亦存在着很多臭虫，因为这并不是件容易的事。
所谓的形式验证因而数学要领描述电脑程式运作时可以接受的「绑定」（bounds），且证明它绝不会超出这些绑定。这是个复杂的程序，因而多数只使用在描绘程式功能的高阶图式（schema）上，将这些图式转换成程式码可能会带来相干验证未能解决的种种复杂问题。
MIT研究职员则是直接验证档案系统的程式码，而非高阶图式，他们透过名为Coq的验证助理工具，以其形式言语描述电脑系统的各个组件与它们之间的关联。由于此一形式验证环境包罗了程式言语，在此环境中以异样的言语撰写档案系统，就能让验证程序检查真正的程式码而非图式。
研究职员先以Coq的形式言语界说此一档案系统的种种元件，然后还得描述这些元件在遭遇当机环境时的举动与彼此间的关联，之后才举行系统验证，并写出绝对应的档案系统。
此一新的档案系统将能包管利用者不会因为系统当掉而遗失资料，纵然受限于今日的尺度而使得该档案系统运作缓慢，但研究职员声称他们所利用的技术将可适用于更细密的设计，形式验证终极将让打造可靠及有用率的档案系统变得更容易。
- 文章作者: 福州军威计算机技术有限公司
军威网络是福州最专业的电脑维修公司,专业承接福州电脑维修、上门维修、IT外包、企业电脑包年维护、局域网网络布线、网吧承包等相关维修服务。
版权声明：原创作品，允许转载，转载时请务必以超链接形式标明文章原始出处 、作者信息和声明。否则将追究法律责任。
TAG:
|
评论加载中...
|
上一篇: 新的Linux档案系统Bcachefs
