Speaker
Description
In this work, we present a formal mathematical model and software library for modelling hardware components and software systems based on the SOPN Petri network and CSharp programming language.
A discrete stochastic model denoted as SOPN, is presented, which combines the qualities of coloured, hierarchical and generalized Petri nets. The model is a series of extensions over the necessary apparatus of stochastic Petri nets, which allows a direct transition from the SOPN model to the basic model of stochastic Petri nets.
Several additional terms were introduced into the model to describe the grouping of elements of the hierarchy of service systems components. The paper presents some theorems that show the resulting models' significant properties from the point of view of the possibilities of their composition. The developed model has many new properties for describing complex computing systems based on Petri nets. So, for example, messages in service systems can be split into packets, some of which are lost and recovered during transmission. On the receiver's side, the packages must be collected back into a single message.
To accomplish this task, it is necessary to support an important property new for Petri nets: decomposition and merging of data elements-labels. This, in turn, requires the ability to identify tags, presented in the proposed SOPN model.
To work correctly with complex data types, the model allows us to consider various levels of the logic of interaction between system components and simulate potential software and hardware levels' potential problems.
A method for organizing an object model based on Petri nets for modelling software systems was created, based on the division of the graph of the logic of operations on elements and their storage locations. The presented method makes it possible to solve the posed problem while maintaining backward compatibility with the model of stochastic Petri nets. Based on the obtained solution, it is possible to represent intricate HPC applications interaction patterns.
To model natural systems within the presented logic framework, a methodology was developed for assessing the performance and identifying bottlenecks of a distributed service system, taking into account potential infrastructure problems.
The reliability of the model is confirmed by the correspondence of the constructed discrete models' behaviour to the analytical indicators for the Amdahl and Gustavsson laws. The paper presents an example of testing the system on the MPI architecture of an application running on a cluster with the Fat Tree architecture and changing its behaviour when varying network equipment errors.
Summary
Precomputation formal verification of HPC cluster applications using SOPN Petri nets in the form of a simple programmable CSharp library
