检索结果-南通市图书馆

基于类C语言内存模型的复杂数据结构验证方法

在线全文

学校读者我要写书评

暂无评论

计算机技术与发展 2024年第8期34卷 57-66页

作者：李薛剑王俊宜安徽大学计算机科学与技术学院安徽合肥230601

对系统中操作复杂结构程序的正确性验证是保证软件高可信的重要途径,目前大多数基于高层抽象建模和程序结构拆分的方法难以满足复杂数据结构程序的验证要求。针对这一问题,论文提出基于类C语言内存模型的验证方法。首先,以内存块为基础... 详细信息

对系统中操作复杂结构程序的正确性验证是保证软件高可信的重要途径,目前大多数基于高层抽象建模和程序结构拆分的方法难以满足复杂数据结构程序的验证要求。针对这一问题,论文提出基于类C语言内存模型的验证方法。首先,以内存块为基础将复杂数据结构的操作进行函数形式的定义和描述,形式化描述内存对象操作性质;其次,针对程序层定义了符合复杂结构描述的文法和语义,并基于符号化的程序逻辑进行推理。实验对嵌入式操作系统内核μC/OS-III中的复杂数据结构进行分析和自动化验证,断言描述和验证条件脚本通过了自动定理证明器的求解。

关键词：形式化验证复杂数据结构程序逻辑内存模型操作系统内核

在线全文

学校读者我要写书评

暂无评论

部分冗余删除的证明变换研究

小型微型计算机系统 2017年第1期38卷 15-19页

作者：李薛剑中国科技大学计算机科学与技术学院合肥230026 安徽大学计算机科学与技术学院合肥230601

部分冗余删除优化是一个同时包含有公共子表达式删除和表达式提升的复杂优化,但是对基于部分冗余删除优化的证明变换研究,还停留在对一些简单情况的处理和讨论上.本文在实验室前期优化对证明调整的研究基础上,总结简单优化行为对证明变... 详细信息

部分冗余删除优化是一个同时包含有公共子表达式删除和表达式提升的复杂优化,但是对基于部分冗余删除优化的证明变换研究,还停留在对一些简单情况的处理和讨论上.本文在实验室前期优化对证明调整的研究基础上,总结简单优化行为对证明变换的调整过程,通过将部分冗余删除优化细分为简单的PRE、复杂的PRE、复制代码的PRE、前瞻的PRE,给出了不仅是简单的优化调整证明方法,而是包含有基于复杂的部分冗余删除优化的证明变换的方法.

关键词：部分冗余删除编译器优化证明变换携带证明的代码

一种对集群回填作业调度改进的RB＿HAR策略

在线全文

学校读者我要写书评

暂无评论

实验室研究与探索 2018年第9期37卷 126-130,137页

作者：李薛剑雷政安徽大学计算机科学与技术学院合肥230601 中国科学技术大学计算机科学与技术学院合肥230026

作为最常用的作业调度策略之一,回填算法被广泛应用于高性能集群作业管理中。之前的工作针对回填算法提出了一些改进策略,提升了集群系统的性能。但由于回填过程是基于作业的预约运行时间进行的,其中对作业运行时间的不准确预估可能导... 详细信息

作为最常用的作业调度策略之一,回填算法被广泛应用于高性能集群作业管理中。之前的工作针对回填算法提出了一些改进策略,提升了集群系统的性能。但由于回填过程是基于作业的预约运行时间进行的,其中对作业运行时间的不准确预估可能导致预约作业未完成或资源浪费。提出的RB_HAR策略与一般回填算法或一些改进的回填算法相比,该算法能有效的提高回填作业的完成率。设计实验将改进的回填算法RB_HAR应用于高性能集群并与先来先服务、一般回填算法对比。实验结果表明,改进的回填算法在继承了回填算法低响应比、高利用率等优点的基础上,进一步提升了回填作业的完成率。

关键词：并行调度预约回填动态预留高性能计算集群

在线全文

学校读者我要写书评

暂无评论

一种基于动态优先级的RQ作业调度算法

小型微型计算机系统 2017年第1期38卷 124-128页

作者：李薛剑李凯中国科学技术大学计算机科学与技术学院合肥230026 安徽大学计算机科学与技术学院合肥230601

传统FCFS调度算法虽然易于实现,但未能解决紧急作业等待问题;而传统优先级调度算法在保证紧急作业优先完成的情况下,对一般作业极不公平.依据此两种调度策略,提出一种基于动态优先级驱动的RQ(Rank Queue)作业调度算法,合理解决优先级和... 详细信息

传统FCFS调度算法虽然易于实现,但未能解决紧急作业等待问题;而传统优先级调度算法在保证紧急作业优先完成的情况下,对一般作业极不公平.依据此两种调度策略,提出一种基于动态优先级驱动的RQ(Rank Queue)作业调度算法,合理解决优先级和公平性之间的矛盾.该算法将作业划分为四个等级,并依次分配到预先设置的4个等待队列上,等待队列设置不同的优先级阈值.动态调整优先级,达到阈值后提升到就绪队列.实验表明:RQ算法在提高资源利用率的同时大大缩短了高优先级作业的响应时间.

关键词：等级等待队列优先级阈值动态优先级

在线全文

学校读者我要写书评

暂无评论

基于DTPS算法的异构集群优化策略

实验室研究与探索 2016年第3期35卷 126-129页

作者：李薛剑陈豪朱凯安徽大学计算机科学与技术学院安徽合肥230601

随着高性能计算机的发展,一种基于CPU-GPU的异构集群逐渐被人们所关注。相比于传统集群,它更经济环保,且拥有更高的运算速度。但异构模式下效率较低的短板也限制着异构集群的发展。本文提出的DTPS算法,通过动态调整异构集群下CPU与GPU... 详细信息

随着高性能计算机的发展,一种基于CPU-GPU的异构集群逐渐被人们所关注。相比于传统集群,它更经济环保,且拥有更高的运算速度。但异构模式下效率较低的短板也限制着异构集群的发展。本文提出的DTPS算法,通过动态调整异构集群下CPU与GPU任务划分的比例,整合集群计算资源,使集群的计算效率达到相对较高的水平,并通过实验证明了算法的有效性。

关键词：异构集群任务划分任务调度动态调整

在线全文

学校读者我要写书评

暂无评论

面向集群的系统性能可视化监控平台

实验室研究与探索 2018年第3期37卷 127-130页

作者：李薛剑胡月月余雪莉安徽大学计算机科学与技术学院合肥230601 安徽科技贸易学校安徽蚌埠233000

伴随着计算机技术的不断发展,对于系统服务稳定性的要求显得尤为重要,集群的监控必不可少。设计并实现一个面向Linux集群的系统性能监控管理器,以检测集群运行状态。该监控管理器采用C/S(客户端/服务器)模式,通过多线程技术完成数据采... 详细信息

伴随着计算机技术的不断发展,对于系统服务稳定性的要求显得尤为重要,集群的监控必不可少。设计并实现一个面向Linux集群的系统性能监控管理器,以检测集群运行状态。该监控管理器采用C/S(客户端/服务器)模式,通过多线程技术完成数据采集处理、缓存技术实现数据查询和HTTP协议完成数据传输,并以可视化图形界面实时显示系统当前状态和对历史数据的查看,同时当系统某一参数超出正常指标,可远程处理瓶颈,以确保系统服务的稳定性。

关键词：集群监控 C/S模式多线程缓存 HTTP协议可视化

高性能计算平台在高校中的应用及服务模式探索

在线全文

学校读者我要写书评

暂无评论

电脑知识与技术 2015年第12X期11卷 42-43页

作者：李薛剑安徽大学计算机科学与技术学院安徽合肥230039 安徽大学高性能计算中心安徽合肥230039

该文论述了高性能计算平台作为开放性的计算资源,在高校环境中如何以服务用户为宗旨,为用户提供高性能计算及专业技术服务。文章从服务模式、科研创新、人才培养、平台的推广等多个方面,阐述了平台在高校中的定位及应当发挥的作用。

关键词：高性能计算服务模式人才培养

3D_EW在MIC并行编程中的移植与实现研究

在线全文

学校读者我要写书评

暂无评论

实验室研究与探索 2017年第4期36卷 123-126页

作者：李薛剑罗京鲁昶许兴中安徽大学计算机科学与技术学院合肥230601

3D_EW是一款用于石油勘探领域的应用程序,其运行需要极高的计算能力支持,在CPU上进行大规模计算时效率极低,而MIC卡为英特尔公司推出的基于集成中和架构的至强融核产品,可以提供数百个同时运行的硬件线程,带来极高的并行性。将3D_EW程... 详细信息

3D_EW是一款用于石油勘探领域的应用程序,其运行需要极高的计算能力支持,在CPU上进行大规模计算时效率极低,而MIC卡为英特尔公司推出的基于集成中和架构的至强融核产品,可以提供数百个同时运行的硬件线程,带来极高的并行性。将3D_EW程序并行化并移植于MIC卡,实验表明:3D_EW进行大规模运算时在MIC并行运行速度远大于仅利用CPU时的串行运行速度。

关键词：三维弹性波建模(3DEW) MIC 移植并行优化策略

对安徽大学图书馆计算机网络系统建设的分析与思考

在线全文

学校读者我要写书评

暂无评论

农业图书情报学刊 2008年第9期20卷 33-35,45页

作者：李薛剑安徽大学计算机学院安徽大学图书馆合肥230039

通过分析安徽大学图书馆的需求,介绍了该馆计算机网络系统具体建设的合理之处,指出了图书馆计算机网络系统建设过程中所应重视的地方,同时也对该系统的不足作出了分析和思考。

关键词：大学图书馆计算机网络系统