基于树状线性规划搜索的单调速率优化设计

来源：软件学报杂志2015年第12期北京时间：

作者：陈力,王永吉,吴敬征,吕荫润

单位：陈力，中国科学院软件研究所基础软件国家工程研究中心, 北京 100190;中国科学院大学, 北京 10004911,王永吉，中国科学院软件研究所基础软件国家工程研究中心, 北京 100190;计算机科学国家重点实验室(中国科学院软件研究所), 北京 100190;中国科学院软件研究所互联网软件技术实验室, 北京 10019002,吴敬征，中国科学院软件研究所基础软件国家工程研究中心, 北京 100190;计算机科学国家重点实验室(中国科学院软件研究所), 北京 10019003,吕荫润，中国科学院软件研究所基础软件国家工程研究中心, 北京 100190;中国科学院大学, 北京 10004904

摘要：改善单调速率(rate monotonic,简称RM)可调度性判定算法的效率,是过去40年计算机实时系统设计的重要问题.最近,研究人员把可调度性判定问题扩展到了更一般的优化设计问题,即,如何调节在区间可选择情况下的任务运行时间,使得:(1)系统RM可调度;(2)系统的某个性能(如CPU利用率)达到最优.在已有的求解实时系统RM优化设计问题的方法中,都是先把原问题建模成广义约束优化问题,然后再对广义约束优化问题进行求解.但现有方法的求解速度较慢,任务数较多时不再适用.提出一种求解优化问题的方法——基于树状的线性规划搜索(linearprogramming search,简称LPS)方法.该方法先将实时系统RM优化设计问题建模成广义约束优化问题,再将其分拆成若干线性规划子问题,然后构造线性规划搜索树,利用剪枝搜索算法求解部分线性规划子问题,最后得到优化解.实验结果表明:LPS方法相比于已有的方法能够节省20%~70%的求解时间,任务数越多,节省时间越多.该研究成果可以与计算机可满足性模定理(satisfiability modulo theories,简称SMT)领域的多个研究热点问题联系起来,并可望改善SMT问题的求解效率.

关键词：实时系统;单调速率;最优化;搜索算法;线性规划;可满足性模定理

基金资助：国家自然科学基金(61170072);国家青年科学基金(61303057);中国科学院、国家外国专家局创新团队国际合作伙伴计划