Thread Algebra with Multi-Level Strategies

• Autorzy: Bergstra J.A. , Middelburg C.A.
• Języki publikacji: EN

Abstrakty

EN

In a previous paper, we developed an algebraic theory about threads and multi-threading based on the assumption that a deterministic interleaving strategy determines how threads are interleaved. The theory includes interleaving operators for a number of plausible deterministic interleaving strategies. The interleaving of different threads constitutes a multi-thread. Several multi-threads may exist concurrently on a single host in a network, several host behaviors may exist concurrently in a single network on the internet, etc. In the current paper, we assume that the above-mentioned kind of interleaving is also present at these other levels. We extend the theory developed so far with features to cover the multi-level case. We use the resulting theory to develop a simplified formal representation schema of systems that consist of several multi-threaded programs on various hosts in different networks. We also investigate the connections of the resulting theory with the algebraic theory of processes known as ACP.

Słowa kluczowe

EN

thread; multi-thread; host; network; service; thread algebra; strategic interleaving; thread-service composition; delayed processing; exception handling; formal design prototype; process algebras

• Wydawca: IOS Press
• Czasopismo: Fundamenta Informaticae
• Rocznik: 2006
• Tom: Vol. 71, nr 2,3
• Strony: 153--182
• Opis fizyczny: tab., bibliogr. 21 poz.

Twórcy

autor

Bergstra J.A.

autor

Middelburg C.A.

• Programming Research Group University of Amsterdam Amsterdam, the Netherlands,

Bibliografia

• [1] Ábrahám, E., de Boer, F. S., de Roever, W. P., Steffen, M.: A Compositional Operational Semantics for JavaMT, Verification: Theory and Practice (N. Dershowitz, Ed.), LNCS 2772, Springer-Verlag, 2003, 290-303.
• [2] Aceto, L., Fokkink,W. J., Verhoef, C.: Structural Operational Semantics, in: Handbook of Process Algebra (J. A. Bergstra, A. Ponse, S. A. Smolka, Eds.), Elsevier, Amsterdam, 2001, 197-292.
• [3] Arnold, K., Gosling, J.: The Java Programming Language, Addison-Wesley, 1996.
• [4] Baeten, J. C. M., Bergstra, J. A.: On Sequential Composition, Action Prefixes and Process Prefix, Formal Aspects of Computing, 6, 1994, 250-268.
• [5] Bergstra, J. A., Bethke, I.: Polarized Process Algebra and Program Equivalence, Proceedings 30th ICALP (J. C. M. Baeten, J. K. Lenstra, J. Parrow, G. J. Woeginger, Eds.), LNCS 2719, Springer-Verlag, 2003, 1-21.
• [6] Bergstra, J. A., Klop, J. W.: Process Algebra for Synchronous Communication, Information and Control, 60(1/3), 1984, 109-137.
• [7] Bergstra, J. A., Klop, J. W.: Process Algebra: Specification and Verification in Bisimulation Semantics, Proceedings Mathematics and Computer Science II (M. Hazewinkel, J. K. Lenstra, L. G. L. T. Meertens, Eds.), CWI Monograph 4, North-Holland, 1986, 61-94.
• [8] Bergstra, J. A., Loots, M. E.: Program Algebra for Sequential Code, Journal of Logic and Algebraic Programming, 51(2), 2002, 125-156.
• [9] Bergstra, J. A., Middelburg, C. A.: Model Theory for Process Algebra, in: Processes, Terms and Cycles: Steps on the Road to Infinity (A. Middeldorp, V. van Oostrom, F. van Raamsdonk, R. C. de Vrijer, Eds.), LNCS 3838, Springer-Verlag, 2005, 445-495.
• [10] Bergstra, J. A., Middelburg, C. A.: Thread Algebra for Strategic Interleaving, Computer Science Report 04-35, Department of Mathematics and Computer Science, Eindhoven University of Technology, November 2004.
• [11] Bergstra, J. A., Middelburg, C. A.: Simulating Turing Machines on Maurer Machines, Computer Science Report 05-28, Department of Mathematics and Computer Science, Eindhoven University of Technology, November 2005.
• [12] Bergstra, J. A., Middelburg, C. A.: Splitting Bisimulations and Retrospective Conditions, Computer Science Report 05-03, Department of Mathematics and Computer Science, Eindhoven University of Technology, January 2005.
• [13] Bergstra, J. A., Middelburg, C. A.: Strong Splitting Bisimulation Equivalence, CALCO 2005 (J. L. Fiadeiro, N. Harman, M. Roggenbach, J. Rutten, Eds.), LNCS 3629, Springer-Verlag, 2005, 85-99.
• [14] Bergstra, J. A., Middelburg, C. A.: A Thread Algebra with Multi-Level Strategic Interleaving, CiE 2005 (S. B. Cooper, B. Löwe, L. Torenvliet, Eds.), LNCS 3526, Springer-Verlag, 2005, 35-48.
• [15] Bergstra, J. A., Ponse, A.: Combining Programs and State Machines, Journal of Logic and Algebraic Programming, 51(2), 2002, 175-192.
• [16] Bishop, J., Horspool, N.: C# Concisely, Addison-Wesley, 2004.
• [17] Brookes, S. D., Hoare, C. A. R., Roscoe, A. W.: A Theory of Communicating Sequential Processes, Journal of the ACM, 31(3), 1984, 560-599.
• [18] Flanagan, C., Freund, S. N., Qadeer, S., Seshia, S. A.: Modular Verification of Multithreaded Programs, Theoretical Computer Science, 338(1/3), 2005, 153-183.
• [19] Middelburg, C. A.: An Alternative Formulation of Operational Conservativity with Binding Terms, Journal of Logic and Algebraic Programming, 55(1/2), 2003, 1-19.
• [20] Milner, R.: A Calculus of Communicating Systems, LNCS 92, Springer-Verlag, Berlin, 1980.
• [21] Stärk, R. F.: Formal Specification and Verification of the C# Thread Model, Theoretical Computer Science, 343, 2005, 482-508.