Modular Verification of SPARCv8 Code

来源 :计算机科学技术学报(英文版) | 被引量 : 0次 | 上传用户:yishaphoto123456
下载到本地 , 更方便阅读
声明 : 本文档内容版权归属内容提供方 , 如果您对本文有版权争议 , 可与客服联系进行内容授权或下架
论文部分内容阅读
Inline assembly code is common in system software to interact with the underlying hardware platforms. The safety and correctness of the assembly code is crucial to guarantee the safety of the whole system. In this paper, we propose a practical Hoare-style program logic for verifying SPARC (Scalable Processor Architecture) assembly code. The logic supports modular reasoning about the main features of SPARCv8 ISA (instruction set architecture), including delayed control transfers, delayed writes to special registers, and register windows. It also supports relational reasoning for refinement verification. We have applied it to verify that there is a contextual refinement between a context switch routine in SPARCv8 and a switch primitive. The program logic and its soundness proof have been mechanized in Coq.
其他文献
CrFeNi2V0.5Wx (x=0,0.25) alloys based on these parameters of mixing enthalpy (△Hmix),mixing entropy (△Smix),atomic radius difference (δ),valance electron con
笔者在少数民族地区从事英语教学十多年了,发现边远地区的学生,英语成绩和城市的学生相比差距较大。边远地区学生英语成绩和城市的学生相比,差距为什么这么大?学生在学习英语
1.麦芽 麦芽较玉米和燕麦更易于吸收,能降低结肠癌和直肠癌发病率。 2.洋葱和大蒜 虽气味不佳,但可防止高血压,降低胆固醇,减少心脏病的发病率。 3.草莓 它可改善皮肤质地,
2020年10月23日,2020年中国稀土行业协会抛光材料分会年会暨中国稀土抛光材料产业发展论坛在苏州成功召开,本次会议以“更高精度更快速度”为主题,来自抛光材料分会会员企业
期刊
In order to better understand why the corrosion behavior of carbon steel exposed in Nansha atmospheric environment is very serious,the effect of sodium,potassiu
目前模拟、数字和混合电路集成到同一衬底的IC非常普遍,在混合信号系统中,模拟电路信号的可观察性有所降低,模拟测试成为系统成本的主要问题,基于DSP的模拟测试仪由于精度高、速
会议
2020年11月3日~4日,中国稀土行业协会副会长兼秘书长杨文浩、常务副秘书长王晓铁等一行,走访了厦门钨业股份有限公司,与公司董事长黄长庚、总裁吴高潮、副总裁钟可祥等领导进
期刊
人们常常把行动的因果性与人的自由当作两个难以相容的基本观念,在当代哲学伦理学中,这两种观念又以“因果空间”和“理由空间”的隐喻得到更为系统的表现,成为现代伦理学发
通过超声波在空气中传播的基本原理,以超声波传感器为接口部件,应用FPGA技术对空气中三维风的风速和风向进行测量,从而设计了一套超声波风速测量系统。对系统硬件组成、测量原理
会议
我国于2004年进行了第一次全国经济普查。普查对象包括在我国境内从事房地产业全部法人单位、产业活动单位和个体经营户。普查主要内容包括房地产单位基本属性、就业人员、财