SpaceWire-D的调度表生成方法
|
摘要
针对航天高速SpaceWire-D提出了一种调度表生成方法。该方法基于贪婪算法和SMT求解器。贪婪算法是主体,在每次迭代中以调度表的分布均匀性为优化原则产生一个约束集作为SMT求解器的输入参数,然后调用SMT求解器。SMT求解器是重要工具,用于对输入参数的可满足性进行判定,如果可满足则将输出的模型作为生成的调度表。此外,还提出了设置分片长度、确定时间槽大小以及划分冲突域的策略。最后,通过试验对方法的效果进行了验证。结果表明,生成调度表的时间较短且调度表具有良好的分布均匀性。
Being aimed at high-speed SpaceWire-D, a method of schedule generation was put forward, implemented with greedy algorithm combined with SMT-Solver. The greedy algorithm was designed to generate a set of constraint for SMT-Solver and to make the frames and frame chips distribute more uniformly in the generated schedule. The SMT-Solver is an important tool and its function is to determine the satisfiability of input parameters. If it is satisfiable, the output module is the schedule wanted. In addition, new policies were proposed about setting the length of frame chips, the size of time-slots, and collision area division. The method was verified with experiments. The results show that the generation algorithm can acquire a schedule featured by approximate uniform distribution in hundreds of milliseconds.
Being aimed at high-speed SpaceWire-D, a method of schedule generation was put forward, implemented with greedy algorithm combined with SMT-Solver. The greedy algorithm was designed to generate a set of constraint for SMT-Solver and to make the frames and frame chips distribute more uniformly in the generated schedule. The SMT-Solver is an important tool and its function is to determine the satisfiability of input parameters. If it is satisfiable, the output module is the schedule wanted. In addition, new policies were proposed about setting the length of frame chips, the size of time-slots, and collision area division. The method was verified with experiments. The results show that the generation algorithm can acquire a schedule featured by approximate uniform distribution in hundreds of milliseconds.
引文
[1] HU K,JIANG H, NIU J W. The design and implementation of high speed manchester II bus physical interface[C]. 2010 International Conference on Computer,Mechatronics,Control and Electronic Engineering(CMCE).Changchun:IEEE,2010:456-459.
[2] 吴中杰, 刘江澜, 宋伟, 等. 可抢占实时星载SpaceWire总线网络研究[J]. 中国空间科学技术, 2016, 36 (6):62-69. WU Z J, LIU J L, SONG W, et al. A pre-emptible real-time spacewire on-board network[J]. Chinese Space Science and Technology, 2016, 36(6):62-69 (in Chinese).
[3] GIBSON D, PARKES S, MCCLEMENTS C, et al. Space-Wire-D prototype and demonstration system[C]. SpaceWire Conference .Yokohama:IEEE, 2016:1-7.
[4] 于广良, 杨孟飞, 徐建, 等. 面向多级中断系统的任务最差响应时间分析[J]. 中国空间科学技术, 2016, 36(2):28-36. YU G L, YANG M F, XU J, et al. Worst case response time analysis of multi-level interrupt system[J]. Chinese Space Science and Technology, 2016, 36(2):28-36 (in Chinese).
[5] 陈英武, 方炎申, 顾中舜. 中继卫星单址链路调度模型与算法研究[J]. 中国空间科学技术, 2007, 27(2):52-58. CHEN Y W, FANG Y S, GU Z S. Algorithms for the single access link scheduling model of tracking and data relay satellite system[J]. Chinese Space Science and Technology, 2007, 27(2):52-58 (in Chinese).
[6] CRACIUNAS S S, OLIVER R S. SMT-based task- and network-level static schedule generation for time-triggered networked systems[C]//Proceedings of the 22nd International Conference on Real-Time Networks and Systems.New York:ACM,2014:45-54.
[7] DUTERTRE B.Yices 2.2[C].26th International Conference on Computer-aided Verification (CAV′2014).Vienna:Springer,2014:737-744.
[8] MOURA L D, BJ?RNER N. Z3: an efficient SMT solver[J], Lecture Notes in Computer Science, 2008, 4963(1):337-340.
[9] HUANG J, BLECH J O, RAABE A, et al. Static sche-duling of a time-triggered network-on-chip based on SMT solving[C]//Proceedings of Design, Automation & Test in Europe Conference & Exhibition. Piscataway: IEEE Press, 2012:509-514.
[10] 徐晓飞, 曹晨, 郭骏, 等. TT-RMS: 时间触发网络通信表生成算法[J]. 北京航空航天大学学报, 2015, 41 (8):1403-1408. XU X F, CAO C, GUO J, et al. TT-RMS: communication table generation algorithm of time-triggered network[J]. Journal of Beijing University of Aeronautics and Astronautics, 2015, 41(8):1403-1408 (in Chinese).
[11] 张超, 南建国, 褚文奎, 等. 改进的TT-RMS调度表生成算法[J]. 空军工程大学学报(自然科学版), 2016, 17 (6):82-87. ZHANG C, NAN J G, CHU W K, et al. An improved communication table generation algorithm based on time-triggered rate monotonic scheduling[J]. Journal of Air Force Engineering University (Natural Science Edition), 2016, 17 (6):82-87 (in Chinese).
[12] 姜宏, 杨孟飞, 刘波, 等. 高速SpaceWire光纤总线系统研究与实现[C]. 2017年全国工业控制计算机年会.北京:中国计算机学会,2017:27-31. JIANG H, YANG M F, LIU B, et al. Research and implementation of high-speed fiber bus system[C]. 2017 China Industrial Control Computer Conference. Beijing:CCF, 2017:27-31(in Chinese).
[13] BAKER T P,SHAW A. The cyclic executive model and ada [C]//The Proceedings of IEEE Real-Time Systems Symposium.Huntsville:IEEE, 1988:120-129.
[14] GHASEMZADEH H,JAFARI R.A greedy buffer allocation algorithm for power-aware communication in body sensor networks[C].2010 International Conference on Hardware/Software Codesign and System Synthesis(CODES+ISSS).Scottsdale:ACM,2010:195-204.
[15] BRUMMAYER R, BIERE A, LONSING F. BTOR: bit-precise modeling of word-level problems for model checking[C]. First International Workshop on Bit-Precise Reasoning.New Jersey:ACM,2008:53-64.
[16] MOK A K, WANG W. Window-constrained real-time periodic task scheduling[C]//Proceedings of IEEE Real-Time Systems Symposium.London:IEEE, 2001:15-24.
[2] 吴中杰, 刘江澜, 宋伟, 等. 可抢占实时星载SpaceWire总线网络研究[J]. 中国空间科学技术, 2016, 36 (6):62-69. WU Z J, LIU J L, SONG W, et al. A pre-emptible real-time spacewire on-board network[J]. Chinese Space Science and Technology, 2016, 36(6):62-69 (in Chinese).
[3] GIBSON D, PARKES S, MCCLEMENTS C, et al. Space-Wire-D prototype and demonstration system[C]. SpaceWire Conference .Yokohama:IEEE, 2016:1-7.
[4] 于广良, 杨孟飞, 徐建, 等. 面向多级中断系统的任务最差响应时间分析[J]. 中国空间科学技术, 2016, 36(2):28-36. YU G L, YANG M F, XU J, et al. Worst case response time analysis of multi-level interrupt system[J]. Chinese Space Science and Technology, 2016, 36(2):28-36 (in Chinese).
[5] 陈英武, 方炎申, 顾中舜. 中继卫星单址链路调度模型与算法研究[J]. 中国空间科学技术, 2007, 27(2):52-58. CHEN Y W, FANG Y S, GU Z S. Algorithms for the single access link scheduling model of tracking and data relay satellite system[J]. Chinese Space Science and Technology, 2007, 27(2):52-58 (in Chinese).
[6] CRACIUNAS S S, OLIVER R S. SMT-based task- and network-level static schedule generation for time-triggered networked systems[C]//Proceedings of the 22nd International Conference on Real-Time Networks and Systems.New York:ACM,2014:45-54.
[7] DUTERTRE B.Yices 2.2[C].26th International Conference on Computer-aided Verification (CAV′2014).Vienna:Springer,2014:737-744.
[8] MOURA L D, BJ?RNER N. Z3: an efficient SMT solver[J], Lecture Notes in Computer Science, 2008, 4963(1):337-340.
[9] HUANG J, BLECH J O, RAABE A, et al. Static sche-duling of a time-triggered network-on-chip based on SMT solving[C]//Proceedings of Design, Automation & Test in Europe Conference & Exhibition. Piscataway: IEEE Press, 2012:509-514.
[10] 徐晓飞, 曹晨, 郭骏, 等. TT-RMS: 时间触发网络通信表生成算法[J]. 北京航空航天大学学报, 2015, 41 (8):1403-1408. XU X F, CAO C, GUO J, et al. TT-RMS: communication table generation algorithm of time-triggered network[J]. Journal of Beijing University of Aeronautics and Astronautics, 2015, 41(8):1403-1408 (in Chinese).
[11] 张超, 南建国, 褚文奎, 等. 改进的TT-RMS调度表生成算法[J]. 空军工程大学学报(自然科学版), 2016, 17 (6):82-87. ZHANG C, NAN J G, CHU W K, et al. An improved communication table generation algorithm based on time-triggered rate monotonic scheduling[J]. Journal of Air Force Engineering University (Natural Science Edition), 2016, 17 (6):82-87 (in Chinese).
[12] 姜宏, 杨孟飞, 刘波, 等. 高速SpaceWire光纤总线系统研究与实现[C]. 2017年全国工业控制计算机年会.北京:中国计算机学会,2017:27-31. JIANG H, YANG M F, LIU B, et al. Research and implementation of high-speed fiber bus system[C]. 2017 China Industrial Control Computer Conference. Beijing:CCF, 2017:27-31(in Chinese).
[13] BAKER T P,SHAW A. The cyclic executive model and ada [C]//The Proceedings of IEEE Real-Time Systems Symposium.Huntsville:IEEE, 1988:120-129.
[14] GHASEMZADEH H,JAFARI R.A greedy buffer allocation algorithm for power-aware communication in body sensor networks[C].2010 International Conference on Hardware/Software Codesign and System Synthesis(CODES+ISSS).Scottsdale:ACM,2010:195-204.
[15] BRUMMAYER R, BIERE A, LONSING F. BTOR: bit-precise modeling of word-level problems for model checking[C]. First International Workshop on Bit-Precise Reasoning.New Jersey:ACM,2008:53-64.
[16] MOK A K, WANG W. Window-constrained real-time periodic task scheduling[C]//Proceedings of IEEE Real-Time Systems Symposium.London:IEEE, 2001:15-24.