一种多核系统任务调度算法动态度量方法
|
摘要
任务调度算法的优劣直接影响系统的功能和性能,对其进行功能验证和性能评价具有很强的现实意义。改进了IMC构建多核系统任务调度算法的功能模型,扩展aCSL从逻辑层次上刻画任务调度算法的性能指标,并基于改进的IMC和扩展的aCSL提出了一种多核系统任务调度算法动态度量方法实现对任务调度算法的功能验证和性能评价。用例分析表明提出的动态度量方法能有效地对任务调度算法进行功能和性能的描述及度量,为多核系统任务调度算法的正确执行提供了有力支撑。
Task scheduling algorithm directly affects the function and performance of the system. The functional verification and performance evaluation of scheduling algorithm have strong practical significance. This paper proposed a novel dynamic measurement method to verify the algorithm's function and performance. It used the improved IMC model to construct the algorithm's function model. It used the extended aCSL to describe the algorithm's performance indicator. Based on the improved IMC and extended aCSL,the proposed method realized the functional verification and performance evaluation of the algorithm. The case study shows that the proposed method can effectively describe and measure the algorithm's function and performance,and can provide powerful support for the correct execution of the algorithm.
Task scheduling algorithm directly affects the function and performance of the system. The functional verification and performance evaluation of scheduling algorithm have strong practical significance. This paper proposed a novel dynamic measurement method to verify the algorithm's function and performance. It used the improved IMC model to construct the algorithm's function model. It used the extended aCSL to describe the algorithm's performance indicator. Based on the improved IMC and extended aCSL,the proposed method realized the functional verification and performance evaluation of the algorithm. The case study shows that the proposed method can effectively describe and measure the algorithm's function and performance,and can provide powerful support for the correct execution of the algorithm.
引文
[1] Kling P,Macker A,Riechers S,et al. Sharing is caring:multiprocessor scheduling with a sharable resource[C]//Proc of the 29th ACM Symposium on Parallelism in Algorithms and Architectures. New York:ACM Press,2017:123-132.
[2] Jain D,Jain S C. Load balancing real-time periodic task scheduling algorithm for multiprocessor enviornment[C]//Proc of International Conference on Circuit,Power and Computing Technologies. Piscataway:IEEEPress,2015:1-5.
[3] O’Regan G. Concise guide to software engineering:from fundamentals to application methods[M].[S. l.]:Springer International Publishing,2017.
[4] Newcombe C,Rath T,Zhang Fan,et al. How Amazon Web services uses formal methods[J]. Communications of the ACM,2015,58(4):66-73.
[5] Bartoletti M,Degano P,Ferrari G L,et al. Model checking usage policies[J]. Mathematical Structures in Computer Science,2015,25(3):710-763.
[6] Boca P P,Bowen J P,Siddiqi J I. Formal methods:state of the art and new directions[M]. London:Springer-Verlag,2010.
[7] Park G L. Performance evaluation of a list scheduling algorithm in distributed memory multiprocessor systems[J]. Future Generation Computer Systems,2004,20(2):249-256.
[8] Manolache S,Eles P,Peng Zebo. Schedulability analysis of multiprocessor real-time applications with stochastic task execution times[C]//Proc of IEEE/ACM International Conference on Computer Aided Design. New York:ACM Press,2003:699-706.
[9] Neuhausser M R,Zhang Lijun. Time-bounded reachability probabilities in continuous-time Markov decision processes[C]//Proc of the7th International Conference on Quantitative Evaluation of Systems.Washington DC:IEEE Computer Society,2010:209-218.
[10] Hillston J,Tribastone M,Gilmore S. Stochastic process algebras:from individuals to populations[J]. Computer Journal,2012,55(7):866-881.
[11] Clark A,Gilmore S,Hillston J,et al. Stochastic process algebras[C]//Formal Methods for Performance Evaluation. Berlin:Springer,2007:132-179.
[12]Gilmore S,Hillston J,Tribastone M,et al. Fluid rewards for a stochastic process algebra[J]. IEEE Trans on Software Engineering,2012,38(4):861-874.
[13]Pereyra M. Proximal Markov chain Monte Carlo algorithms[J]. Statistics and Computing,2016,26(4):745-760.
[14]Guck D,Han T,Katoen J P,et al. Quantitative timed analysis of interactive Markov chains[C]//Proc of International Conference on NASA Formal Methods. Berlin:Springer,2012:8-23.
[15]Conlisk J. A stability theorem for an interactive Markov chain[J].Journal of Mathematical Sociology,2010,6(1):163-168.
[16]吴尽昭,王永祥,覃广平.交互式马尔可夫链——并发系统的设计、验证与评价[M].北京:科学出版社,2007.(Wu Jinzhao,Wang Yongxiang,Qin Gangping. Interactive Markov chains:design,verification and evaluation for concurrent system[M]. Beijing:Science Press,2007.)
[2] Jain D,Jain S C. Load balancing real-time periodic task scheduling algorithm for multiprocessor enviornment[C]//Proc of International Conference on Circuit,Power and Computing Technologies. Piscataway:IEEEPress,2015:1-5.
[3] O’Regan G. Concise guide to software engineering:from fundamentals to application methods[M].[S. l.]:Springer International Publishing,2017.
[4] Newcombe C,Rath T,Zhang Fan,et al. How Amazon Web services uses formal methods[J]. Communications of the ACM,2015,58(4):66-73.
[5] Bartoletti M,Degano P,Ferrari G L,et al. Model checking usage policies[J]. Mathematical Structures in Computer Science,2015,25(3):710-763.
[6] Boca P P,Bowen J P,Siddiqi J I. Formal methods:state of the art and new directions[M]. London:Springer-Verlag,2010.
[7] Park G L. Performance evaluation of a list scheduling algorithm in distributed memory multiprocessor systems[J]. Future Generation Computer Systems,2004,20(2):249-256.
[8] Manolache S,Eles P,Peng Zebo. Schedulability analysis of multiprocessor real-time applications with stochastic task execution times[C]//Proc of IEEE/ACM International Conference on Computer Aided Design. New York:ACM Press,2003:699-706.
[9] Neuhausser M R,Zhang Lijun. Time-bounded reachability probabilities in continuous-time Markov decision processes[C]//Proc of the7th International Conference on Quantitative Evaluation of Systems.Washington DC:IEEE Computer Society,2010:209-218.
[10] Hillston J,Tribastone M,Gilmore S. Stochastic process algebras:from individuals to populations[J]. Computer Journal,2012,55(7):866-881.
[11] Clark A,Gilmore S,Hillston J,et al. Stochastic process algebras[C]//Formal Methods for Performance Evaluation. Berlin:Springer,2007:132-179.
[12]Gilmore S,Hillston J,Tribastone M,et al. Fluid rewards for a stochastic process algebra[J]. IEEE Trans on Software Engineering,2012,38(4):861-874.
[13]Pereyra M. Proximal Markov chain Monte Carlo algorithms[J]. Statistics and Computing,2016,26(4):745-760.
[14]Guck D,Han T,Katoen J P,et al. Quantitative timed analysis of interactive Markov chains[C]//Proc of International Conference on NASA Formal Methods. Berlin:Springer,2012:8-23.
[15]Conlisk J. A stability theorem for an interactive Markov chain[J].Journal of Mathematical Sociology,2010,6(1):163-168.
[16]吴尽昭,王永祥,覃广平.交互式马尔可夫链——并发系统的设计、验证与评价[M].北京:科学出版社,2007.(Wu Jinzhao,Wang Yongxiang,Qin Gangping. Interactive Markov chains:design,verification and evaluation for concurrent system[M]. Beijing:Science Press,2007.)