Abstract
Event-B is a tool-supported specification language that can be used e.g. for modelling of concurrent programs. This calls for code generation and a means of executing the resulting code. One approach is to preserve the original event-based nature of the model and use a run-time scheduler and message passing to execute the translated events on different computational nodes. In this paper, we consider the efficiency of such a solution when applied to a compute-intensive model. In order to mitigate overhead, we also use a method allowing computational nodes to repeat event execution without the involvement of the scheduler. To find out under what circumstances the approach performs most efficiently, we perform an empirical study with different parameters.
This research was supported by the EU funded FP7 project DEPLOY (214158). http://www.deploy-project.eu
Chapter PDF
Similar content being viewed by others
References
Abrial, J.-R.: Modeling in Event-B: System and Software Engineering. Cambridge University Press (2010)
Abrial, J.-R., Butler, M., Hallerstede, S., Voisin, L.: An Open Extensible Tool Environment for Event-B. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 588–605. Springer, Heidelberg (2006)
Degerlund, F., Grönblom, R., Sere, K.: Code generation and scheduling of Event-B models. Technical report, Turku Centre for Computer Science, TUCS (2011)
GNU Compiler Collection (GCC) web site, http://gcc.gnu.org/
Grönblom, R.: A framework for code generation and parallel execution of Event-B models. Master’s thesis, Åbo Akademi University (2009)
Hallerstede, S.: On the purpose of Event-B proof obligations. Formal Aspects of Computing 23, 133–150 (2011)
Message Passing Interface forum, http://www.mpi-forum.org/
MPICH2 web site, http://www.mcs.anl.gov/research/projects/mpich2/
Wright, S.: Using EventB to Create a Virtual Machine Instruction Set Architecture. In: Börger, E., Butler, M., Bowen, J.P., Boca, P. (eds.) ABZ 2008. LNCS, vol. 5238, pp. 265–279. Springer, Heidelberg (2008)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 IFIP International Federation for Information Processing
About this paper
Cite this paper
Degerlund, F. (2012). Scheduling of Compute-Intensive Code Generated from Event-B Models: An Empirical Efficiency Study. In: Göschka, K.M., Haridi, S. (eds) Distributed Applications and Interoperable Systems. DAIS 2012. Lecture Notes in Computer Science, vol 7272. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-30823-9_15
Download citation
DOI: https://doi.org/10.1007/978-3-642-30823-9_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-30822-2
Online ISBN: 978-3-642-30823-9
eBook Packages: Computer ScienceComputer Science (R0)