验证带有线程的动态创建和退出的多线程程序

近来在程序验证领域,Feng和Shao提出一个类Hoare逻辑的验证框架以验证包含中断的底层程序.在该工作基础上进行扩展,提出一个验证包含线程的动态创建和退出机制程序的框架.框架包含抽象机器模型、指令规范、逻辑推理系统、框架可靠性定理其证明.框架采用Hoare风格的推导方式,使用高阶逻辑描述指令的推理规则和安全策略,为证明带有线程的动态创建和退出的多线程程序的部分正确性提供了一种实用的方法.

Linux下支持续传的多线程下载工具的设计与实现

介绍了一个在Linux环境下支持续传和多线程下载工具的设计技术,并讨论了在实现中用到的一些数据结构和关键技术。

Linux下通用线程池的改进与实现

对线程池的阻塞唤醒机制,动态调整,线程安全退出,参数处理,系统线程数限制等细节进行研究,保证了其在不同应用场景下的独立性和通用性;同时采用一种基于数组的链表机制来改进线程池的查找分配算法,将其时间复杂度稳定在O(1),避免了传统线程池当线程数目过大时导致的查询分配性能下降的问题。实验结果表明,改进后的线程池与传统的系统线程分配方式相比在开销上有很大节省。