Abstract
In stepwise program development, abstract specifications can be transformed into (parallel) programs which preserve functional correctness. Although tackling bad performance after a program’s deployment may require a costly redesign, deployment decisions are usually made very late in program development. This paper argues for the introduction of deployment decisions as an integrated part of a development-by-construction process: Deployment decisions should be expressed as part of a program’s high-level model and evaluated by how they affect program performance, using metrics at an appropriate level of abstraction. To illustrate such a deployment-by-construction process, we sketch how deployment decisions may be modelled and evaluated, concerning data layout in shared memory for parallel programs targeting shared-memory multicore architectures with caches. For simplicity, we use an abstract metric of data access penalties and simulate data accesses on a memory system which internally ensures data coherency between cores.
Supported by SIRIUS – Centre for Scalable Data Access (www.sirius-labs.no).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
Notes
- 1.
The full approach with the different components can be download from: https://github.com/ShijiBijo84/DbC.
- 2.
Note that a special memory block is reserved for each lock reference, whose value is either 0 or 1, indicating whether a lock is taken.
References
Abrial, J.-R.: The B-Book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)
Aldrich, J., Chambers, C., Notkin, D.: ArchJava: connecting software architecture to implementation. In: Tracz, W., Young, M., Magee, J. (eds.), Proceedings of the 24th International Conference on Software Engineering (ICSE 2002), pp. 187–197. ACM (2002)
Andrews, G.R.: Foundations of Multithreaded, Parallel, and Distributed Programming. Addison Wesley, Reading (2000)
Bac, R., Kurki-Suonio, R.: Decentralization of process nets with centralized control. In: Probert, R.L., Lynch, N.A., Santoro, N. (eds.), Proceedings of the Second Annual ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, pp. 131–142. ACM (1983)
Back, R., Sere, K.: Stepwise refinement of parallel algorithms. Sci. Comput. Program. 13(1), 133–180 (1989)
Back, R.-J.J., Wright, J.V.: Refinement Calculus: A Systematic Introduction, 1st edn. Springer, New York (1998). https://doi.org/10.1007/978-1-4612-1674-2
Balsamo, S., Marco, A.D., Inverardi, P., Simeoni, M.: Model-based performance prediction in software development: a survey. IEEE Trans. Softw. Eng. 30(5), 295–310 (2004)
Bijo, S., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: A formal model of parallel execution in multicore architectures with multilevel caches (long version). Research report, Department of Informatics, University of Oslo (2017). http://violet.at.ifi.uio.no/papers/mc-rr.pdf
Bijo, S., Johnsen, E.B., Pun, K.I., Tapia Tarifa, S.L.: A formal model of parallel execution on multicore architectures with multilevel caches. In: Proença, J., Lumpe, M. (eds.) FACS 2017. LNCS, vol. 10487, pp. 58–77. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68034-7_4
Bijo, S., Pun, K.I., Tapia Tarifa, S.L.: Modelling data access patterns with atomic sections for multicore architectures (long version). Research report, Department of Informatics, University of Oslo (2017). http://violet.at.ifi.uio.no/papers/mc-lock-rr.pdf
Binkert, N., et al.: The gem5 simulator. SIGARCH Comput. Arch. News 39(2), 1–7 (2011)
Carlson, T.E., Heirman, W., Eeckhout, L.: Sniper: exploring the level of abstraction for scalable and accurate parallel multi-core simulation. In: Proceedings of International Conference for High Performance Computing, Networking, Storage and Analysis (SC), pp. 52:1–52:12. ACM (2011)
Chandy, K.M., Misra, J.: Parallel Program Design: A Foundation. Addison-Wesley, Reading (1988)
Chandy, K.M., Taylor, S.: An Introduction to Parallel Programming. Jones and Bartlett, Austin (1991)
Ciccozzi, F., Corcoran, D., Seceleanu, T., Scholle, D.: Smartcore: boosting model-driven engineering of embedded systems for multicore. In: Proceedings of the 12th International Conference on Information Technology - New Generations, pp. 89–94. IEEE Computer Society (2015)
Ciccozzi, F., Feljan, J., Carlson, J., Crnković, I.: Architecture optimization: speed or accuracy? both! Softw. Qual. J., November 2016
Clavel, M., et al.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-71999-1
Culler, D.E., Gupta, A., Singh, J.P.: Parallel Computer Architecture: A Hardware/Software Approach, 1st edn. Morgan Kaufmann Publishers Inc., San Francisco (1997)
Derler, P., Lee, E.A., Sangiovanni-Vincentelli, A.L.: Modeling cyber-physical systems. Proc. IEEE 100(1), 13–28 (2012)
Hähnle, R., Johnsen, E.B.: Designing resource-aware cloud applications. IEEE Comput. 48(6), 72–75 (2015)
Johnsen, E.B., Hähnle, R., Schäfer, J., Schlatte, R., Steffen, M.: ABS: a core language for abstract behavioral specification. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 142–164. Springer, Heidelberg (2011). https://doi.org/10.1007/978-3-642-25271-6_8
Johnsen, E.B., Schlatte, R., Tarifa, S.L.T.: Integrating deployment architectures and resource consumption in timed object-oriented models. J. Log. Algebr. Meth. Program. 84(1), 67–91 (2015)
Kourie, D.G., Watson, B.W.: The Correctness-by-Construction Approach to Programming. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-27919-5
Miller, J.E., et al.: Graphite: a distributed parallel simulator for multicores. In: Proceedings of the 16th International Symposium on High-Performance Computer Architecture (HPCA), pp. 1–12. IEEE Computer Society (2010)
Morgan, C.: Programming from Specifications. Prentice Hall International Series in Computer Science, 2nd edn. Prentice Hall, Upper Saddle River (1994)
Morgan, C.: Programming from Specifications. Prentice-Hall International, Upper Saddle River (1998)
Schmidl, D., Vesterkjær, A., Müller, M.S.: Evaluating OpenMP performance on thousands of cores on the Numascale architecture. In: PARCO, vol. 27 of Advances in Parallel Computing, pp. 83–92. IOS Press (2015)
Solihin, Y.: Fundamentals of Parallel Multicore Architecture, 1st edn. Chapman & Hall/CRC, Boca Raton (2015)
Sorin, D.J., Hill, M.D., Wood, D.A.: A Primer on Memory Consistency and Cache Coherence, 1st edn. Morgan & Claypool Publishers, San Francisco (2011)
Taylor, R.N., Medvidovic, N., Dashofy, E.M.: Software Architecture: Foundations, Theory, and Practice. Wiley Publishing, Hardcover (2009)
van Ommering, R.C., van der Linden, F., Kramer, J., Magee, J.: The Koala component model for consumer electronics software. IEEE Comput. 33(3), 78–85 (2000)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2018 Springer Nature Switzerland AG
About this paper
Cite this paper
Bijo, S., Johnsen, E.B., Pun, K.I., Seidl, C., Tarifa, S.L.T. (2018). Deployment by Construction for Multicore Architectures. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Modeling. ISoLA 2018. Lecture Notes in Computer Science(), vol 11244. Springer, Cham. https://doi.org/10.1007/978-3-030-03418-4_26
Download citation
DOI: https://doi.org/10.1007/978-3-030-03418-4_26
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-03417-7
Online ISBN: 978-3-030-03418-4
eBook Packages: Computer ScienceComputer Science (R0)