臺灣博碩士論文加值系統

隨著在嵌入式系統上所執行的應用其複雜度逐漸增加，這些應用需要更多的計算能力以滿足各種不同效能上的需求，例如即時和資源使用上的限制。傳統在單一處理器的嵌入式系統上，如單處理器晶片系統，其循序式的執行方式已經不能夠應付逐漸增加的應用複雜度；而多處理器晶片系統已經引進了一種新的設計風格以滿足各式各樣不同應用在效能上的需求並且也用來設計具有低必v且即時的嵌入式系統。但為了能夠充分地利用多處理器晶片系統所提供的巨大計算能力和資源，系統必須要能夠根據動態的工作量去自我作調適。因此為了達到較平衡的工作負載、較高的資源使用率、節省能源以及較佳的必v消耗，動態工作遷移的能力必定要被包含在多處理器的晶片系統中。在此系統中支援動態工作遷移的能力，提供某種彈性使得系統可以滿足更多應用的需求；然而卻也進一步地增加系統設計的複雜度，並使得系統行為和其效能在分析上變得更加地難以預測。因此為了能確保在這樣具有動態工作遷移能力之多處理器晶片系統中時間和資源使用上的正確性並且能夠分析其系統的行為，一個驗證的方法論是極為必要的。在本篇論文中，我們針對系統層級且具有動態工作遷移能力的多處理器晶片系統，提出一個有效率的合作式驗證方法論。此方法論透過結合模擬和模型檢驗這兩種常用的驗證技術，來驗證在此多處理器晶片系統中時間和資源使用上的相關議題。而藉由此合作式的驗證方法論，我們能夠在模擬及模型檢驗此兩種方法中取得在時間和空間上較佳的平衡。進而，此方法論可以幫助系統做更聰明的動態工作遷移、且減緩狀態空間爆炸對驗證上的影響、並且也適合去驗證具有動態變化行為的系統或較大型的系統。

With the complexity of applications running on the embedded systems increases gradually, applications need more computational power to meet different performance demands such as real-time and resource usage constraints. Traditionally, the sequential execution paradigm in single processor embedded systems, like single processor Systems-on-Chip (SoC), can no longer cope with the increasing application complexity. Multiprocessor SoC (MPSoC) has introduced a new design style to meet various application performance requirements and to design low-power and real-time embedded systems. For fully utilizing the vigorous computing power and resources, the system must be able to adapt itself to a dynamic workload. As a consequence, to achieve better load balancing, better utilization of resources, energy saving, and more power efficient, task migration capabilities must be involved in MPSoC systems. Supporting run-time task migration in MPSoC provides the flexibility to meet more application requirements yet further increasing the system design complexity and making the system analysis more unpredictable. Therefore, a verification methodology is imperative for ensuring the correctness in timing and in resource usage and analyzing the behavior of MPSoC systems while supporting run-time task migration. In this work, we propose an efficient collaborative verification methodology for system level MPSoC systems with run-time task migration. We combine two well-known verification techniques, namely simulation and model checking, for verifying the timing and resource usage issues of the MPSoC systems with run-time task migration consideration. By applying the collaborative verification methodology, we can get better tradeoff between time and space that inherently hindered from simulation and model checking. Furthermore, the proposed methodology can make more intelligent task migration, alleviate the impact of the state space explosion problem, and suit to verify the systems of dynamic change behavior and larger systems. Application examples show the feasibility and benefits of the proposed collaborative verification methodology of MPSoC system with supporting run-time task migration capability.

1 Introduction 1
1.1 Design Challenges . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3
1.2 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5
1.3 Proposed Solution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9
1.4 Thesis Organization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14
2 Related Work 15
2.1 Task Migration in MPSoC . . . . . . . . . . . . . . . . . . . . . . . . . . 15
2.2 Verification of SoC and MPSoC . . . . . . . . . . . . . . . . . . . . . . . 22
3 Preliminaries 31
3.1 System Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
3.2 Task Model . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37
3.3 Property Definition . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40
3.4 Assumptions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 43
3.5 Target Problem and Solution . . . . . . . . . . . . . . . . . . . . . . . . . 44
4 Efficient Collaborative Verification Methodology 47
4.1 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47
4.2 Collaborative Interface . . . . . . . . . . . . . . . . . . . . . . . . . . . . 51
4.3 Model Checking Phase . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53
4.4 Simulation Phase . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55
4.5 Collaborative Verification . . . . . . . . . . . . . . . . . . . . . . . . . . . 58
5 Experiment Environment and Application Examples 62
5.1 Experiment Environment . . . . . . . . . . . . . . . . . . . . . . . . . . . 62
5.2 Application Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 64
5.2.1 Designed Example . . . . . . . . . . . . . . . . . . . . . . . . . . 65
5.2.2 Different Migration Mechanisms . . . . . . . . . . . . . . . . . . . 75
6 Conclusions and Future Work 80
Bibliography 80

[1] SystemC 2.2 library. http://www.systemc.org/.
[2] SystemC v2.0.1 Functional Spec. http://www.systemc.org/.
[3] SystemC v2.0.1 Users Guide. http://www.systemc.org/.
[4] R. Alur and D. L. Dill. A theory of timed automata. Theoretical Computer Science., 126(2):183–235, April 1994.
[5] T. Amnell, E. Fersman, L. Mokrushin, P. Pettersson, andW. Yi. TIMES - A Tool for Modelling and Implementation of Embedded Systems. In Proceedings of the 8th International Conference
on Tools and Algorithms for the Construction and Analysis of Systems (TACAS’02), pages 460–464. Springer-Verlag, April 2002.
[6] G. Behrmann, A. David, and K. G. Larsen. A Tutorial on UPPAAL. In Formal Methods for the Design of Real-Time Systems: 4th International School on Formal Methods for the Design of Computer, Communication, and Software Systems, SFM-RT, LNCS, pages 200–236. Springer–Verlag, September 2004.
[7] S. Bertozzi, A. Acquaviva, D. Bertozzi, and A. Poggiali. Supporting Task Migration in Multi-Processor Systems-on-Chip: A Feasibility Study. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE), pages 15–20. IEEE Computer Society, March 2006.
[8] A. Brekling. Modelling and Verification of MPSoC. Master’s thesis, Informatics and Mathematical Modelling, Technical University of Denmark, DTU, Kongens Lyngby, October 2006.
[9] A. Brekling, M. R. Hansen, and J. Hansen. A Timed Automata Semantics for a System-Level MPSoC Model. In Proceedings of the 18th Nordic Workshop on Programming Theory (NWPT’06). Reykjavik University, October 2006.
[10] E. W. Briao, D. Barcelos, F. Wronski, and F. R. Wagner. Impact of Task Migration in NoCbased MPSoCs for Soft Real-time Applications. In Proceedings of the IFIP International Conference on Very Large Scale Integration, Lecture Notes in Computer Science, pages 296–299. Springer, October 2007.
[11] E. Carvalho, N. Calazans, and F. Moraes. Heuristics for Dynamic Task Mapping in NoC-based Heterogeneous MPSoCs. In Proceedings of the 18th IEEE/IFIP International Workshop on Rapid System Prototyping (RSP), pages 34–40. IEEE Computer Society, May 2007.
[12] E. M. Clarke and E. A. Emerson. Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. In Logic of Programs, volume 131, pages 52–71. Springer-Verlag, May 1981.
[13] E. M. Clarke, E. A. Emerson, and A. P. Sistla. Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Transactions on Programming Languages and Systems (TOPLAS), 8(2):244–263, April 1986.
[14] E. M. Clarke, O. Grumberg, and D. A. Peled. Model Checking. MIT Press, 1999.
[15] S. Dutta, R. Jensen, and A. Rieckmann. Viper: A Multiprocessor SOC for Advanced Set-Top Box and Digital TV Systems. IEEE Design and Test of Computers, 18(5):21–31, September/October 2001.
[16] J. Ellebæk, K. S. Knudsen, A. Brekling, M. R. Hansen, and J. Madsen. MOVES - A tool for Modeling and Verification of Embedded Systems. In DATE’07 University Booth, April 2007.
[17] P. Flake, S. Davidmann, and F. Schirrmeister. System-Level Exploration Tools for MPSoC Designs. In Proceedings of the 43rd Annual Design Automation Conference (DAC), pages 286–287. ACM Press, July 2006.
[18] N. Guan, Z. Gu, Q. Deng, S. Gao, and G. Yu. Exact Schedulability Analysis for Static-Priority Global Multiprocessor Scheduling Using Model-Checking. In Proceedings of the 5th IFIP WG 10.2 International Workshop, Software Technologies for Embedded and Ubiquitous Systems, Lecture Notes in Computer Science, pages 263–272. Springer, May 2007.
[19] J. Helmig. Developing core software technologies for TI’s OMAPTM platform, Available at http://www.ti.com/. 2002.
[20] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine. Symbolic Model Checking for Real-Time Systems. In Proceedings of 7th. Symposium of Logics in Computer Science, pages 394–406, Santa-Cruz, California, September 1992. IEEE Computer Scienty Press.
[21] P.-A. Hsiung, Y.-R. Chen, and Y.-H. Lin. Model Checking Safety-Critical Systems Using Safecharts. IEEE Transactions on Computers, 56(5):692–705, May 2007.
[22] P.-A. Hsiung, S.-W. Lin, Y.-R. Chen, C.-H. Huang, J.-J. Yeh, H.-Y. Sun, C.-S. Lin, and H.-W. Liao. Model Checking Timed Systems with Urgencies. In Proceedings of the 4th International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 4218 of LNCS, pages 67–81. Springer-Verlag, October 2006.
[23] P.-A. Hsiung and F. Wang. A state-graph manipulator tool for real-time system specification and verification. In Proceedings of the 5th International Conference on Real-Time Computing Systems and Applications (RTCSA’98), pages 181–188, October 1998.
[24] P.-A. Hsiung and F.Wang. User-friendly verification. In Proceedings of the IFIP TC6/WG6.1 Joint International Conference on Formal Description Techniques For Distributed Systems and Communication Protocols Protocol Specification, Testing, And Verification, (FORTE/PSTV’99), pages 279–294, October 1999.
[25] Intel. Product Brief: Intel IXP 2850 Network Processor, Available at
http://www.intel.com/design/network/prodbrf/25213601.pdf. 2002.
[26] Y. Jegou. Runtime support for task migration on distributed memory architectures. In Proceedings of IPPS Workshop on run-time systems for parallel programming (RTSPP’97), pages 41–50, April 1997.
[27] A. A. Jerraya, A. Bouchhima, and F. P´etrot. Programming models and HW-SW Interfaces Abstraction for Multi-Processor SoC. In Proceedings of the 43rd Annual Design Automation Conference (DAC), pages 280–285. ACM Press, July 2006.
[28] A. A. Jerraya, H. Tenhunen, and W. Wolf. Guest Editors’ Introduction: Multiprocessor Systems-on-Chips. IEEE Computer, 38(7):36–40, 2005.
[29] Kim Guldstrand Larsen, Paul Pettersson, and Wang Yi. UPPAAL in a Nutshell. International Journal on Software Tools for Technology Transfer, 1(1-2):134–152, 1997.
[30] LEGOS−TEAM. The LegOS Homepage. http://legos.sourceforge.net. 2002.
[31] W.-S. Liao and P.-A. Hsiung. Creating a Formal Verification Platform for IBM CoreConnectbased SoC. In Proceedings of the 1st International Workshop on Automated Technology for Verification and Analysis (ATVA 2003), pages 7–18, December 2003.
[32] W.-S. Liao and P.-A. Hsiung. FVP: A formal verification platform for SoC. In Proceedings of the 16th IEEE International SoC Conference, pages 21–24. IEEE Circuits and Systems Society, September 2003.
[33] W.-S. Liao and P.-A. Hsiung. Modeling Hardware Systems with Complex Clock Synchronizations in the SGM Formal Verifier. In Proceedings of the VLSI Design / CAD Symposium, pages 177–180, Hwalien, Taiwan, August 2003.
[34] S.-W. Lin, P.-A. Hsiung, C.-H. Huang, and Y.-R. Chen. Model Checking Prioritized Timed Automata. In Proceedings of the 3rd International Symposium on Automated Technology for Verification and Analysis (ATVA), volume 3707 of LNCS, pages 370–384. Springer-Verlag, October 2005.
[35] M. Litzkow and M. Livny. Supporting Checkpointing and Process Migration Outside the UNIX Kernel. In Proceedings of the Winter 1992 USENIX Conference, pages 283–290, San Francisco, CA, January 1992. ACM Press/Addison-Wesley Publishing Co.
[36] S. Mahadevan, M. Storgaard, J. Madsen, and K. Virk. ARTS: A System-Level Framework for Modeling MPSoC Components and Analysis of their Causality. In Proceedings of the 13th IEEE International Symposium on Modeling, Analysis, and Simulation of Computer and Telecommunication Systems (MASCOTS’05), pages 480–483. IEEE Computer Society, September 2005.
[37] G. Martin. Overview of the MPSoC design challenge. In Proceedings of the 43rd Annual Design Automation Conference (DAC), pages 274–279. ACM Press, July 2006.
[38] D. S. Milojiˇci´c, F. Douglis, Y. Paindaveine, R. Wheeler, and S. Zhou. Process Migration Survey. ACM Computing Surveys (CSUR), 32(3):241–299, September 2000.
[39] D. S. Milojiˇci´c and Y. Paindaveine. Process vs. Task Migration. In Proceedings of the 29th Hawaii International Conference on System Sciences (HICSS’96) Volume 1: Software Technology and Architecture, pages 636–645. IEEE Computer Society Press, January 1996.
[40] G. E. Moore. Cramming More Components onto Integrated Circuit. Electronics, 38(8):114–117, April 1965.
[41] M. D. Nava, P. Blouet, P. Teninge, M. Coppola, T. Ben-Ismail, S. Picchiottino, and R.Wilson. An Open Platform for Developing Multiprocessor SoCs. IEEE Computer, 38(7):60–67, 2005.
[42] R. D. Nelson and M. S. Squillante. Modeling and Analysis of Task Migration in Shared-Memory Multiprocessor Computer Systems. In Proceedings of the 4th International Workshop on Modeling, Analysis, and Simulation of Computer and Telecommunications Systems (MASCOTS’96), pages 261–266. IEEE Computer Society, February 1996.
[43] J. E. Nielsen and K. S. Knudsen. MoVES - A tool for Modelling and Verification of Embedded Systems. Master’s thesis, Informatics and Mathematical Modelling, Technical University of Denmark, DTU, Kongens Lyngby, April 2007.
[44] V. Nollet, P. Avasare, J-Y. Mignolet, and D. Verkest. Low Cost Task Migration Initiation in a Heterogeneous MP-SoC. In Proceedings of the Conference on Design, Automation and Test in Europe (DATE), pages 252–253. IEEE Computer Society Press, March 2005.
[45] J.-P. Queille and J. Sifakis. Specification and verification of concurrent systems in CESAR. In Proceedings of the 5th Colloquium on International Symposium on Programming, volume 137, pages 337–351. Springer-Verlag, April 1982.
[46] K. Richter, M. Jersak, and R. Ernst. A Formal Approach to MpSoC Performance Verification. IEEE Computer, 36(4):60–67, April 2003.
[47] J. M. Smith. A survey of process migration mechanisms. ACM SIGOPS Operating Systems Review, 22(3):28–40, July 1988.
[48] K. W. Susanto. A Verification Platform for System on Chip. PhD thesis, Department of Computing Science University of Glasgow, Glasgow, UK, October 2003.
[49] F. Wang and P.-A. Hsiung. Efficient and User-Friendly Verification. IEEE Transactions on Computers, 51(1):61–83, January 2002.
[50] W. Wolf. The Future of Multiprocessor Systems-on-Chips. In Proceedings of the 41st Annual Design Automation Conference (DAC), pages 681–685. ACM Press, June 2004.