检索结果-内蒙古大学图书馆

计算机研究与发展 2005年第10期42卷 1802-1808页

作者：廖渊淮晓永李明树中国科学院软件研究所互联网软件技术实验室中国科学院研究生院北京100039 中国科学院软件研究所计算机科学国家重点实验室北京100080

在性能变化不确定的系统内,不同的应用处于竞争和共享有限的系统资源、并受其变化影响的环境中·在系统运行时,对于需要QoS保证的应用,为保证其QoS属性,应能适应于这种环境·考虑到系统资源的全局管理特性,仅从应用中增加适应... 详细信息

在性能变化不确定的系统内,不同的应用处于竞争和共享有限的系统资源、并受其变化影响的环境中·在系统运行时,对于需要QoS保证的应用,为保证其QoS属性,应能适应于这种环境·考虑到系统资源的全局管理特性,仅从应用中增加适应机制是不够的,还需在系统层中增加QoS管理机制·为此,给出了一种面向构件系统的QoS管理模型———QuCOM(qualitycomponent)及其集成到系统构件框架的方法,使基于QuCOM开发的构件应用能够适应于变化的系统环境,并为了验证QuCOM的有效性,以一个视频流应用为例,给出了相关实验数据分析·

关键词：构件模型框架服务质量 QoS管理

来源：评论

学校读者我要写书评

暂无评论

多媒体节目时序描述的组合技术

引用

软件学报 2001年第3期12卷 398-404页

作者：赵琛中国科学院软件研究所计算机科学开放研究实验室北京100080

组合性是形式描述研究的基本问题 ,便于大型程序的设计、分析、测试和复用 .为了方便用户编制大型多媒体系统的时序描述 ,组合模型是必须的 .目前 ,这样的模型有基于语言的、基于图形的、基于时间区间的和面向对象的等等 .但是 ,这些模... 详细信息

组合性是形式描述研究的基本问题 ,便于大型程序的设计、分析、测试和复用 .为了方便用户编制大型多媒体系统的时序描述 ,组合模型是必须的 .目前 ,这样的模型有基于语言的、基于图形的、基于时间区间的和面向对象的等等 .但是 ,这些模型描述层次过低 ,很难支持两个多媒体节目之间的时序描述 .通过引入单位流的概念和扩展两种时序关系 ,研究一种多媒体节目时序描述的结构化技术 ,使复杂的多媒体节目易于理解 ,以方便用户运用组合方法把一些可以复用于不同多媒体节目的节目模块进行组合设计 .

关键词：时序关系时序描述组合多媒体节目软件开发

来源：评论

学校读者我要写书评

暂无评论

有序实数加法理论新的判定过程与多项式谱

引用

软件学报 2001年第7期12卷 1088-1095页

作者：薛锐中国科学院软件研究所计算机科学开放研究实验室北京100080

推广VolkerWeispfenning关于正的有序实数加法理论的量词消去方法 ,得到有序实数加法理论的一个量词消去的判定过程 .在此基础上构造出一个新的、更为精细的判定方法 .并且利用这一结果证明了固定量词长度的子类属于相应计算复杂性的多... 详细信息

推广VolkerWeispfenning关于正的有序实数加法理论的量词消去方法 ,得到有序实数加法理论的一个量词消去的判定过程 .在此基础上构造出一个新的、更为精细的判定方法 .并且利用这一结果证明了固定量词长度的子类属于相应计算复杂性的多项式谱 .与E .D .Sontag的类似结论比较 ,从这种简洁的方式可以得到一个较优的结果 .这个结果实际上将N .Megiddo的关于正实数理论的结论推广到了一般实数理论 .

关键词：判定过程计算复杂性多项式谱有序实数加法理论

来源：评论

学校读者我要写书评

暂无评论

HiLog:OpenHarmony的高性能日志系统

引用

软件学报 2024年第4期35卷 2055-2075页

作者：吴圣垚王枫武延军凌祥屈晟罗天悦吴敬征中国科学院软件研究所智能软件研究中心北京100190 计算机科学国家重点实验室(中国科学院软件研究所) 北京100190

日志是计算机系统中记录事件状态信息的的重要载体,日志系统负责计算机系统的日志生成、收集和输出.OpenHarmony是新兴的、面向全设备、全场景的开源操作系统.在所述工作之前,包括日志系统在内OpenHarmony有许多关键子系统尚未构建,而Op... 详细信息

日志是计算机系统中记录事件状态信息的的重要载体,日志系统负责计算机系统的日志生成、收集和输出.OpenHarmony是新兴的、面向全设备、全场景的开源操作系统.在所述工作之前,包括日志系统在内OpenHarmony有许多关键子系统尚未构建,而OpenHarmony的开源特性使第三方开发者可以为其贡献核心代码.为了解决Open Harmony日志系统缺乏的问题,主要开展如下工作:(1)分析当今主流日志系统的技术架构和优缺点;(2)基于OpenHarmony操作系统的异构设备互联特性设计HiLog日志系统模型规范;(3)设计并实现第1个面向OpenHarmony的日志系统HiLog,并贡献到OpenHarmony主线;(4)对HiLog日志系统的关键指标进行测试和对比试验.实验数据表明,在基础性能方面,HiLog和Log的日志写入阶段吞吐量分别为1500 KB/s和700 KB/s,相比Android日志系统吞吐量提升114%;在日志持久化方面,HiLog可以3.5%的压缩率进行持久化,并且丢包率小于6‰,远低于Log.此外,HiLog还具备数据安全、流量控制等新型实用能力.

关键词：操作系统日志系统开源软件数据安全流量控制

来源：评论

学校读者我要写书评

暂无评论

π-演算互模拟判定算法的优化和实现

引用

软件学报 2001年第2期12卷 159-166页

作者：许文方海林惠民中国科学院软件研究所计算机科学开放研究实验室北京100080

π-演算采用互模拟作为进程等价的准则 .对有限状态的 π-演算进程互模拟等价是可判定的 ,由此提出了互模拟检测算法的一种优化技术 .该技术基于只将输入名字实例化为在以后的等名测试中用到的自由名字 .通过实例说明这一优化技术可大... 详细信息

π-演算采用互模拟作为进程等价的准则 .对有限状态的 π-演算进程互模拟等价是可判定的 ,由此提出了互模拟检测算法的一种优化技术 .该技术基于只将输入名字实例化为在以后的等名测试中用到的自由名字 .通过实例说明这一优化技术可大大减少所用的时间和空间 ,并证明了优化算法的正确性 .

关键词：进程代数 π-演算互模拟验证算法计算机

来源：评论

学校读者我要写书评

暂无评论

嵌套谓词等式系与弱互模拟

引用

软件学报 1999年第11期10卷 1121-1126页

作者：林惠民中国科学院软件研究所计算机科学开放研究实验室北京100080

带赋值符号迁移图是一般传值进程的语义模型，其强互模拟等价可以归结为谓词等式系的最大解．该文将这一结果推广到弱互模拟等价，为此，引入嵌套谓调等式系的概念，并提出算法，将带赋值符号迁移图的弱互模拟等价归结为形如E2μE1的嵌... 详细信息

带赋值符号迁移图是一般传值进程的语义模型，其强互模拟等价可以归结为谓词等式系的最大解．该文将这一结果推广到弱互模拟等价，为此，引入嵌套谓调等式系的概念，并提出算法，将带赋值符号迁移图的弱互模拟等价归结为形如E2μE1的嵌套谓词等式系的最大解．

关键词：传值进程互模拟谓词等式系符号迁移图算法

来源：评论

学校读者我要写书评

暂无评论

由一阶逻辑公式得到命题逻辑可满足性问题实例

引用

软件学报 2005年第3期16卷 327-335页

作者：黄拙张健中国科学院软件研究所计算机科学重点实验室北京100080 中国科学院研究生院北京100039 中国科学院软件研究所计算机科学重点实验室北京100080

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶... 详细信息

命题逻辑可满足性(SAT)问题是计算机科学中的一个重要问题.近年来许多学者在这方面进行了大量的研究,提出了不少有效的算法.但是,很多实际问题如果用一组一阶逻辑公式来描述,往往更为自然.当解释的论域是一个固定大小的有限集合时,一阶逻辑公式的可满足性问题可以等价地归约为SAT问题.为了利用现有的高效SAT工具,提出了一种从一阶逻辑公式生成SAT问题实例的算法,并描述了一个自动的转换工具,给出了相应的实验结果.还讨论了通过增加公式来消除同构从而减小搜索空间的一些方法.实验表明,这一算法是有效的,可以用来解决数学研究和实际应用中的许多问题.

关键词：可满足性问题一阶逻辑命题逻辑

来源：评论

学校读者我要写书评

暂无评论

求解布尔与非线性数值约束相混合的约束问题

引用

软件学报 2005年第5期16卷 659-668页

作者：季晓慧张健中国科学院软件研究所计算机科学重点实验室北京100080 中国科学院研究生院北京100049 中国科学院软件研究所计算机科学重点实验室北京100080

布尔与数值变量相混合的约束问题有着广泛的应用,但是当约束中的数值变量间存在非线性关系时该问题求解起来十分困难.目前的许多求解方法都是不完备的,即这些方法不能完全肯定某些包含非线性数值表达式的约束是否能够成立.针对这种问题... 详细信息

布尔与数值变量相混合的约束问题有着广泛的应用,但是当约束中的数值变量间存在非线性关系时该问题求解起来十分困难.目前的许多求解方法都是不完备的,即这些方法不能完全肯定某些包含非线性数值表达式的约束是否能够成立.针对这种问题,提出了将非线性数值约束转化为特殊形式的优化问题,采用全局优化算法对其进行求解的方法.已经实现了一个基于此方法的原型工具.实验结果表明,该方法能够有效地求解非线性混合约束问题,并且总能够得到该约束条件是否可满足的结果.

关键词：约束求解非线性数值约束全局优化区间方法

来源：评论

学校读者我要写书评

暂无评论

三机冗余容错系统的描述和验证

引用

软件学报 2003年第1期14卷 54-61页

作者：郭亮唐稚松中国科学院软件研究所计算机科学重点研究实验室北京100080

使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessorP刻画程序P在单机上运行,用时序逻辑式SpecP刻画P向外部环境输出的数据所满足的性质.最后证明,采... 详细信息

使用XYZ/E描述和验证三机冗余容错系统.考虑每台计算机加载了一个不断向外界环境输出数据的确定性顺序程序P,用XYZ/E程序SingleProcessorP刻画程序P在单机上运行,用时序逻辑式SpecP刻画P向外部环境输出的数据所满足的性质.最后证明,采用三机冗余模式所得到的程序TripleProcessorsP即使在出现硬件错误的情况下运行,也能满足性质SpecP.

关键词：三机冗余容错系统验证计算机容错性

来源：评论

学校读者我要写书评

暂无评论

SpMV的自动性能优化实现技术及其应用研究

引用

计算机研究与发展 2009年第7期46卷 1117-1126页

作者：袁娥张云泉刘芳芳孙相征中国科学院软件研究所并行计算实验室北京100190 中国科学院研究生院北京100049 中国科学院计算机科学国家重点实验室北京100190

在科学计算中,稀疏矩阵向量乘(SpMV)是一个十分重要且经常被大量调用的计算内核.由于SpMV一般实现算法的浮点计算和存储访问次数比率非常低,且其存储访问模式极为不规则,其实际运行性能往往很低.通过采用寄存器分块算法和启发式分块大... 详细信息

在科学计算中,稀疏矩阵向量乘(SpMV)是一个十分重要且经常被大量调用的计算内核.由于SpMV一般实现算法的浮点计算和存储访问次数比率非常低,且其存储访问模式极为不规则,其实际运行性能往往很低.通过采用寄存器分块算法和启发式分块大小选择算法,将稀疏矩阵分成小的稠密分块,重用保存在寄存器中向量x元素,可以提高该计算内核的性能.剖析和总结了OSKI软件包所采用的若干关键优化技术,并进行了实际应用性能测试.测试表明,在实际应用这些优化技术的过程中,应用程序对SpMV的调用次数要达到上百次的量级,才能抵消由于应用这些性能优化技术所带来的额外时间开销,取得性能加速效果.在Pentium4和AMD Athlon平台上,测试了10个矩阵,其平均加速比分别达到了1.69和1.48.

关键词：稀疏矩阵向量乘启发式算法自适应性能优化存储访问模式寄存器分块

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：