Kronecker Algebra for Static Analysis of Barriers in Ada

详细信息    查看全文

• 关键词：Static program analysis ; Ada tasking ; Synchronization primitives ; Thread synchronization ; Barriers ; Kronecker algebra
• 刊名：Lecture Notes in Computer Science
• 出版年：2016
• 出版时间：2016
• 年：2016
• 卷：9695
• 期：1
• 页码：145-159
• 全文大小：485 KB
• 参考文献：1.Aiken, A., Gay, D., Barrier inference. In: POPL, pp. 342–354 (1998)
  2.Bellman, R.: Introduction to Matrix Analysis. Classics in Applied Mathematics, 2nd edn. Society for Industrial and Applied Mathematics, Philadelphia (1997)MATH
  3.Brukardt, R.L. (ed): Annotated Ada Reference Manual, ISO/IEC 8652:2012(E) with COR.1:2016 (2016). http://​www.​ada-auth.​org/​standards/​aarm12_​w_​tc1/​AA-Final.​pdf
  4.Buchholz, P., Kemper, P.: Efficient computation and representation of large reachability sets for composed automata. Discrete Event Dyn. Syst. 12(3), 265–286 (2002)MathSciNet CrossRef MATH
  5.Burgstaller, B., Blieberger, J.: Kronecker algebra for static analysis of Ada programs with protected objects. In: George, L., Vardanega, T. (eds.) Ada-Europe 2014. LNCS, vol. 8454, pp. 27–42. Springer, Heidelberg (2014)
  6.Burgstaller, B., Scholz, B., Blieberger, J.: A symbolic analysis framework for static analysis of imperative programming languages. J. Syst. Softw. 85(6), 1418–1439 (2012)CrossRef
  7.Davio, M.: Kronecker products and shuffle algebra. IEEE Trans. Comput. 30(2), 116–125 (1981)MathSciNet CrossRef MATH
  8.Downey, A.B.: The Little Book of Semaphores. Green Tea Press, Virginia (2005)
  9.Fechete, R., Kienesberger, G., Blieberger, J.: A framework for CFG-based static program analysis of Ada programs. In: Kordon, F., Vardanega, T. (eds.) Ada-Europe 2008. LNCS, vol. 5026, pp. 130–143. Springer, Heidelberg (2008)CrossRef
  10.González, J.F.: Java 7 Concurrency Cookbook. Packt Publishing Ltd., Birmingham (2012)
  11.Graham, A.: Kronecker Products and Matrix Calculus with Applications. Ellis Horwood Ltd., New York (1981)MATH
  12.Hill, J.M.D., Skillicorn, D.B.: Practical barrier synchronisation. In: PDP, pp. 438–444 (1998)
  13.Kamil, A., Yelick, K.A.: Concurrency analysis for parallel programs with textually aligned barriers. In: Ayguadé, E., Baumgartner, G., Ramanujam, J., Sadayappan, P. (eds.) LCPC 2005. LNCS, vol. 4339, pp. 185–199. Springer, Heidelberg (2006)CrossRef
  14.Kuich, W., Salomaa, A.: Semirings, Automata, Languages. Springer, Heidelberg (1986)CrossRef MATH
  15.Le, D.-K., Chin, W.-N., Teo, Y.-M.: Verification of static and dynamic barrier synchronization using bounded permissions. In: Groves, L., Sun, J. (eds.) ICFEM 2013. LNCS, vol. 8144, pp. 231–248. Springer, Heidelberg (2013)CrossRef
  16.Malkis, A., Banerjee, A.: Verification of software barriers. In: PPoPP (2012)
  17.Mittermayr, R., Blieberger, J.: Shared memory concurrent system verification using Kronecker algebra. Technical report 183/1-155, Automation Systems Group, TU Vienna, September 2011. http://​arxiv.​org/​abs/​1109.​5522
  18.Mittermayr, R., Blieberger, J.: Timing analysis of concurrent programs. In: Vardanega, T. (ed) 12th WCET, vol. 23, pp. 59–68 (2012)
  19.Mittermayr, R., Blieberger, J., Schöbel, A.: Kronecker algebra based deadlock analysis for railway systems. J. PROMET 2012, 359–369 (2012)
  20.Plateau, B.: On the stochastic structure of parallelism and synchronization models for distributed algorithms. In: SIGMETRICS 1985, vol. 13, pp. 147–154 (1985)
  21.Ramalingam, G.: Context-sensitive synchronization-sensitive analysis is undecidable. ACM Trans. Program. Lang. Syst. 22(2), 416–430 (2000)CrossRef
  22.Stefan, M., Blieberger, J., Schöbel, A.: Application of Kronecker algebra in railway operation. Tehnički vjesnik - Technical Gazette (2016, to appear)
  23.Zhang, Y., Duesterwald, E.: Barriers matching for programs with textually unaligned barriers. In: PPoPP, pp. 194–204 (2007)
  24.Zhang, Y., Duesterwald, E., Gao, G.R.: Concurrency analysis for shared memory programs with textually unaligned barriers. In: Adve, V., Garzarán, M.J., Petersen, P. (eds.) LCPC 2007. LNCS, vol. 5234, pp. 95–109. Springer, Heidelberg (2008)CrossRef
  
• 作者单位：Robert Mittermayr (16)
  Johann Blieberger (16)
  
  16. Institute of Computer Aided Automation, Vienna University of Technology, Vienna, Austria
  
• 丛书名：Reliable Software Technologies ¨C Ada-Europe 2016
• ISBN：978-3-319-39083-3
• 刊物类别：Computer Science
• 刊物主题：Artificial Intelligence and Robotics
  Computer Communication Networks
  Software Engineering
  Data Encryption
  Database Management
  Computation by Abstract Devices
  Algorithm Analysis and Problem Complexity
  
• 出版者：Springer Berlin / Heidelberg
• ISSN：1611-3349
• 卷排序：9695

文摘

Kronecker algebra until now has been applied to concurrent programs that use semaphores and protected objects for synchronization. Like many other programming languages, Ada uses barriers, too. In this paper, we present a new synchronization construct for barriers. By applying this, we are able to statically analyze Ada multi-tasking programs that employ barriers for synchronization issues. It turns out that we can use our existing Kronecker algebra implementation completely unmodified for concurrent program graphs using such barrier synchronization primitives.