Repositorio Institucional de Documentos

2013 126 Juan Pablo López Grao Contributions to the deadlock problem in multithreaded software applications observed as Resource Allocation Systems Departamento Director/es Informática e Ingeniería de Sistemas Colom Piazuelo, José Manuel Director/es Tesis Doctoral Autor Repositorio de la Universidad de Zaragoza – Zaguan http://zaguan.unizar.es UNIVERSIDAD DE ZARAGOZA Departamento Director/es Juan Pablo López Grao CONTRIBUTIONS TO THE DEADLOCK PROBLEM IN MULTITHREADED SOFTWARE APPLICATIONS OBSERVED AS RESOURCE ALLOCATION SYSTEMS Director/es Informática e Ingeniería de Sistemas Colom Piazuelo, José Manuel Tesis Doctoral Autor 2013 Repositorio de la Universidad de Zaragoza – Zaguan http://zaguan.unizar.es UNIVERSIDAD DE ZARAGOZA Departamento Director/es Director/es Tesis Doctoral Autor Repositorio de la Universidad de Zaragoza – Zaguan http://zaguan.unizar.es UNIVERSIDAD DE ZARAGOZA Contribuciones al problema de bloqueo en aplicaciones software multihilo abordadas como Sistemas de Asignaci´on de Recursos Juan Pablo L´opez Grao TESIS DOCTORAL Departamento de Inform´atica e Ingenier´ıa de Sistemas Universidad de Zaragoza Director: Jos´e Manuel Colom Piazuelo Julio 2013 Contributions to the deadlock problem in multithreaded software applications observed as Resource Allocation Systems Juan Pablo L´opez Grao PhD THESIS Departament of Computer Science and Systems Engineering University of Zaragoza PhD advisor: Jos´e Manuel Colom Piazuelo July 2013 To Esther (I love you!), to Juan, our little masterpiece (thanks God you resemble Mom!), and to our much-awaited Pablo. Contents Introduction 1 1 Resource Allocation Systems: A facet of Discrete Event Systems 7 1.1 Introduction................................. 8 1.2 The role of abstraction . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.3 The resource allocation problem through Petri net models . . . . . . . 13 1.3.1 An overview of model features . . . . . . . . . . . . . . . . . . 14 1.3.2 Petri net models for RASs . . . . . . . . . . . . . . . . . . . . . 20 1.3.3 Deployment of the RAS vision in different domains . . . . . . . 22 1.4 The class of S4PRnetsystems ...................... 28 1.5 Conclusions................................. 32 2 The resource allocation problem in software applications 33 2.1 Introduction................................. 34 2.2 The RAS view of a software application . . . . . . . . . . . . . . . . . 34 2.3 The PC2Rclass............................... 40 2.3.1 Functional entities. Representation . . . . . . . . . . . . . . . . 40 2.3.2 Definition.............................. 50 2.3.3 Hierarchy of classes and p-semiflows . . . . . . . . . . . . . . . 52 2.3.4 Basic structural properties . . . . . . . . . . . . . . . . . . . . . 54 2.4 A cross-sectional view on the liveness analysis problem . . . . . . . . . 58 2.4.1 Acceptability of the initial marking: The 0-1 zone . . . . . . . 59 2.4.2 Liveness characterisation and siphons . . . . . . . . . . . . . . 66 2.4.3 Deadlock-freeness, liveness, reversibility and livelocks . . . . . . 68 2.5 An insight on the problem of RASs with lender processes . . . . . . . 76 2.5.1 Constructing systems with Plain Lender Processes . . . . . . . 80 2.5.2 The SPQR class: Definition . . . . . . . . . . . . . . . . . . . . 82 2.5.3 The SPQR class: Some structural properties . . . . . . . . . . 83 2.5.4 The SPQR class: Some behavioural properties . . . . . . . . . 86 i ii Contents 2.5.5 Transformations and class relations . . . . . . . . . . . . . . . . 88 2.6 Conclusions................................. 90 3 The liveness problem: Characterisation, analysis and synthesis 95 3.1 Introduction................................. 96 3.2 On siphon-based liveness enforcing in FMSs . . . . . . . . . . . . . . . 97 3.2.1 The synthesis flow for liveness enforcing . . . . . . . . . . . . . 97 3.2.2 Managing siphons for the computation of virtual resources . . . 101 3.2.3 Siphon computation via the resource pruning graph . . . . . . 109 3.2.4 Structural regions and the privatisation of resources . . . . . . 115 3.3 Liveness analysis of PC2R models through siphons . . . . . . . . . . . 130 3.3.1 Towards a liveness characterisation of PC2R models . . . . . . 130 3.3.2 Liveness of PC2R models with 1-acceptable initial markings . . 143 3.3.3 Some properties of siphons in PC2Rnets ............ 146 3.4 A toolbox for synthesising live PC2Rmodels .............. 160 3.4.1 No room for despair: Heuristics to obtain live models . . . . . 160 3.4.2 Divide and conquer: Deconstructing a PC2R model . . . . . . 162 3.4.3 Opening the RAS toolbox: The set of rules . . . . . . . . . . . 166 3.4.4 Fitting the jigsaw together . . . . . . . . . . . . . . . . . . . . 178 3.5 Conclusions................................. 179 4 Reconstructing the Gadara approach 183 4.1 Introduction................................. 184 4.2 TheGadaraapproach ........................... 185 4.3 Liveness characterisation . . . . . . . . . . . . . . . . . . . . . . . . . . 188 4.4 Approaching Gadara by means of S4PRnets .............. 197 4.4.1 A constrained subclass of S4PR with deterministic processes . 197 4.4.2 The conflict expansion rule . . . . . . . . . . . . . . . . . . . . 198 4.4.3 On liveness and siphons preservation . . . . . . . . . . . . . . . 199 4.4.4 Transformation rules between Gadara and CPR nets . . . . . . 203 4.4.5 Synthesis from the underlying CPR net . . . . . . . . . . . . . 204 4.5 Conclusions................................. 208 5 Some complexity results on the resource allocation problem 211 5.1 Introduction................................. 212 5.2 Motivation of the complexity analysis and methodology . . . . . . . . 214 5.3 Ondecidingliveness ............................ 218 5.4 On detecting bad markings . . . . . . . . . . . . . . . . . . . . . . . . 223 5.5 On detecting spurious markings . . . . . . . . . . . . . . . . . . . . . . 228 5.6 Conclusions................................. 229 Contents iii Concluding Remarks 231 A Basic Petri nets notation 235 B Some additional examples and figures 239 Bibliography 246 iv Contents List of Tables 1.1 Modelling capabilities of some well-known Petri net classes for RASs . 23 2.1 Liveness, reversibility and t-semiflow realisability: Combinations . . . 76 2.2 Update of Table 2.1 assuming a 1-acceptable initial marking . . . . . . 77 2.3 Comparison of liveness-related properties among the SnPR family . . 92 3.1 Evaluating Theorem 3.13 for the PC2Rnet in Fig. 3.23 ........ 140 3.2 Evaluating Theorem 3.13 for the S5PR net in Fig. 2.13 ......... 142 v vi List of Tables List of Figures 1.1 Layout of a manufacturing cell . . . . . . . . . . . . . . . . . . . . . . 24 1.2 Layout of a multiprocessor interconnection network . . . . . . . . . . . 25 1.3 Example of deadlock in a tow type AGV transportation system . . . . 27 1.4 Non-live S4PR net system with unemptyable siphons . . . . . . . . . . 30 1.5 Inclusion relations between Petri net classes for RASs ......... 32 2.1 Process subnet model for Algorithm 2.1 (Philosopher 1) . . . . . . . . 36 2.2 PC2Rnet model for Example 2.1 (Postmodern dining philosophers) . 37 2.3 Schematic diagram of an iterative state machine . . . . . . . . . . . . 41 2.4 Elementary iteration blocks of an iterative state machine . . . . . . . . 44 2.5 Shrinking graph of the iterative state machine in Fig. 2.4 ....... 49 2.6 A rather simple PC2Rnet......................... 57 2.7 Partially dead PC2Rnet system with no scarcely marked p-semiflow . 60 2.8 Partially dead PC2Rnet system with misleading spurious markings . . 62 2.9 Live PC2Rnet system with no realisable minimal t-semiflow . . . . . . 63 2.10 The 0-1 zone of acceptable initial markings in PC2Rnets ....... 65 2.11 PC2Rnet proving that liveness is not monotonic at the 0-1 zone . . . 66 2.12 S3PR net proving that liveness is not monotonic . . . . . . . . . . . . 67 2.13 Two postmodern dining philosophers: A non-live S5PR net system . . 69 2.14 Non-live but deadlock-free L-S3PR netsystem.............. 70 2.15 The liveness discontinuity zone in PC2Rnets .............. 71 2.16 Live S5PR net system with no home state . . . . . . . . . . . . . . . . 73 2.17 Reachability graph of the net system in Fig. 2.16 ............ 74 2.18 Live and reversible PC2Rsystem with no realisable minimal t-semiflow 75 2.19 Live PC2Rnet system with no home state . . . . . . . . . . . . . . . . 77 2.20 Reachability graph of the net system in Fig. 2.19 ............ 78 2.21 Non-{live,reversible}PC2Rwith no realisable minimal t-semiflow . . . 79 2.22 Three SPQR nets featuring interesting structural particularities . . . . 85 2.23 Transformation rule: From PC2Rto SB SPQR nets .......... 90 vii viii List of Figures 2.24 From PC2Rto SB SPQR nets: Two postmodern dining philosophers . 91 2.25 Inclusion relations between Petri net classes for RASs (update 1) . . . 93 3.1 A non-live S4PR net system to be controlled . . . . . . . . . . . . . . 101 3.2 Applying Algorithm 3.1 on the net in Fig. 3.1 .............. 106 3.3 A non-live net system with a non-convex permissible marking space . 107 3.4 Applying Algorithm 3.1 on the net in Fig. 3.3 .............. 108 3.5 A non-live S3PR net ............................ 110 3.6 Reachability graph of the net system in Fig. 3.5 ............. 111 3.7 Resource pruning graph Gof the net in Fig. 3.5 ............. 112 3.8 Controlled version of the net in Fig. 3.5 ................. 113 3.9 Illustrating diverse synthesis approaches through a non-live S3PR net 117 3.10 Structural regions (s-regs) of a SOAR2net................ 121 3.11 Order relation between the s-regs of a SOAR2net ........... 122 3.12 Agglomerated resource pruning graph of the SOAR2net in Fig. 3.11 .123 3.13 A non-live SOAR2net and its corresponding resource pruning graph . 125 3.14 Pruning graph of the s-regs of the net in Fig. 3.13 ........... 126 3.15 The net of Fig. 3.13 after enforcing liveness by resource privatisation . 127 3.16 Structural regions of the net in Fig. 3.5 ................. 128 3.17 Pruning graph of the s-regs of the net in Fig. 3.5 ............ 128 3.18 Pruning graphs of the net in Fig. 3.5 after enforcing liveness . . . . . . 129 3.19 Controlled version of the net in Fig. 3.5 ................. 130 3.20 Reachability graph of the live net system in Fig. 3.19 .......... 131 3.21 A live PC2Rnet system within ‘the gap’ . . . . . . . . . . . . . . . . . 134 3.22 A live S5PR net system within ‘the gap’ . . . . . . . . . . . . . . . . . 135 3.23 A non-live PC2Rnet system within ‘the gap’ . . . . . . . . . . . . . . 139 3.24 Minimal siphons that are not covered by any minimal p-semiflow . . . 156 3.25 PC2Rnet: Every minimal siphon is covered by a minimal p-semiflow . 158 3.26 A p-semiflow ysuch that no minimal siphon contains kyk ∩ PR.... 159 3.27 Decomposition of a PC2Rnetmodel................... 163 3.28 Process splitting: Transforming the net in Fig. 2.13 ........... 168 3.29 Rule 2: P-semiflow cancellation . . . . . . . . . . . . . . . . . . . . . . 170 3.30 The net of Fig. 3.23 after applying Rule 2 on A0, B0 and C2 . . . . . 171 3.31 Decomposition of the net in Fig. 3.28 in subsystems . . . . . . . . . . 175 3.32 Subsystem 1 of the net system in Fig. 3.31 ................ 176 3.33 Controlled version of the net in Fig. 3.28 ................. 177 3.34 Controlled version of the net in Fig. 2.13 ................. 180 4.1 Inclusion relations between Petri net classes for RASs (update 2) . . . 185 4.2 Non-live Gadara net system . . . . . . . . . . . . . . . . . . . . . . . . 187 List of Figures ix 4.3 Non-live controlled Gadara net system with no bad minimal siphon . 194 4.4 Gadara net for which some non-minimal siphon must be controlled . . 195 4.5 Controlled Gadara net corresponding to the net in Fig. 4.4 ...... 196 4.6 Example of a conflict expansion in a Gadara net . . . . . . . . . . . . 199 4.7 Transformation of the net in Fig. 4.2 into a CPR net.......... 200 4.8 The CPR net obtained after controlling siphon D0of Fig. 4.7 ..... 206 4.9 The CPR net obtained after extending arcs in the net of Fig. 4.8 ... 207 4.10 After applying the last transformation: The corrected Gadara net . . 208 5.1 Layout of a video streaming system . . . . . . . . . . . . . . . . . . . . 215 5.2 S4PR net system which models the system in Fig. 5.1 ......... 216 5.3 Deadlocked S4PR net system illustrating the system state in Fig. 5.1 .217 5.4 SAT →S4PR-NL. Net Nj ifor each literal xiin Cj............ 220 5.5 SAT →S4PR-NL. Example: F=x1(x1+x2)(x2+x3). ........ 222 5.6 SAT →S4PR-RIM. Net Nj ifor each literal xiin Cj........... 226 5.7 SAT →S4PR-RIM. Example: F=x2(x1+x2)x2. ........... 228 A.1 Transformation rule: Removing self-loop places . . . . . . . . . . . . . 236 B.1 Reachability graph of the PC2Rnet in Fig 2.6 ............. 240 B.2 Resource pruning graph of the PC2Rnet in Fig 2.6 ........... 240 B.3 Resource pruning graph of the PC2Rnet in Fig. 2.21 .......... 241 B.4 S-reg pruning graph of Fig. 3.11, including labels . . . . . . . . . . . . 242 B.5 Agglomerated resource pruning graph of Fig. 3.12, including labels . . 242 B.6 Resource pruning graph of the net in Fig. 3.22 ............. 243 B.7 Resource pruning graph of the net in Fig. 3.23 ............. 243 B.8 Resource pruning graph of the net in Fig. 3.24 ............. 244 B.9 Reachability graph of the net in Fig. 3.26 ................ 245 B.10 Resource pruning graph of the net in Fig. 3.26 ............. 245 xList of Figures Introduction 3 coexist, and these must compete in order to be granted the allocation of some shared resources. Deadlocks arise when a set of processes is indefinitely waiting for resources that are already held by other processes of the same set [CES71]. From a qualitative standpoint, the Resource Allocation Problem (RAP) consists in meeting the demand for resources of the set of processes while dealing with the set of potential system deadlocks. Petri nets constitute a fertile ground to deal with such deadlocks. Many real-world RASs can be abstracted into a conceptualisation constructed around two entities: processes and resources. Petri nets are constructively simple models which feature an appealing graphical representation for modelling these abstractions [Col03]. Besides, there exist powerful structural results for certain subclasses of Petri nets for RASs which enable powerful analysis and synthesis techniques for identifying and fixing potential or factual deadlocks [ECM95,PR01,TGVCE05]. In the end, the corrections computed for the model are deployed over the real-world system. This methodology has been successfully applied to Flexible Manufacturing Systems (FMSs) where processes follow predefined production plans and resources can be artifacts such as robots, machines or conveyor belts, or passive elements such as storage area. Diverse classes of Petri net models, such as System of Simple Sequential Processes with Resources (S3PR) [ECM95], S4PR [PR01,TGVCE05] and many others [JXP02,XJ99] were defined for this aim, with specific attributes for modeling different configurations of FMSs. However, all of them prove insufficient for modelling the RAP in multithreaded software [LGC12]. Nevertheless, the structure of this category of RASs introduces new challenges due to the particularities of programming languages which will be addressed in the following chapters. In short, the main goal of the thesis is to provide a profound and more general insight on the liveness problem in RASs with sequential processes and serially reusable resources, particularly from the perspective of dealing with multithreaded software correction. This includes the proposal of a Petri net-based design methodology, the review and integration of previous results in the new framework, the production of efficient liveness analysis algorithms for the new Petri net class, as well as the proposition of efficient methods for overcoming deadlock problems in the real system. The theoretical complexity of various aspects related to the RAP will also be explored and heuristics and relaxations will be proposed to alleviate that computational complexity. The thesis is organised as follows: 1. A major problem in the literature with regard to the study of the RAP using Petri nets is the disparity of proposed models, often with a strong overlap in terms of its modeling capability. In Chap. 1, a state of the art review is addressed and enriched through the establishment of taxonomic categories that allow capturing the different capabilities of each kind of model. Thus, the 4Introduction groundwork is laid to shed light on the shortcomings of each of these models on fully capturing the RAS vision of multithreaded software. This is materialised in the next chapter. 2. The modelling needs of this kind of systems are discussed in Chap. 2. As a result, a new class of Petri nets, named Processes Competing for Conservative Resources (PC2R), is introduced. The PC2Rclass provides a framework in which the above results are adequately encompassed and expanded. This completes the map of the RASs with sequential processes and resources used conservatively. Moreover, a categorisation of the intrinsic structural and behavioural properties of PC2Rand subclasses is conducted in the chapter. Unlike for other wellknown classes such as free choice nets [Hil85], a direct relationship between the deadlock-freeness property (i.e., the enabling of at least one transition is ever granted) and system liveness (i.e., no transition is ever dead) does not generally exist in the context of RASs. Thus, it is possible to find nets in which some transitions are dead while other parts of the net can normally progress. This is true for almost all known Petri net models for RASs, except for very restricted subclasses. This and other properties (non-directedness, existence of home states, etc.) are characteristic of the new models and delimit the difficulties to be found in this kind of systems to implement earlier results or provide efficient solutions to the RAP. In this chapter, the properties that affect liveness in PC2Rnets are studied in depth, as well as how they extrapolate (or not) to its subclasses. Additionally, transformation rules that allow us to study this kind of systems throughout syntactically simpler models are introduced. 3. Chapter 3tackles the analysis and synthesis of multithreaded software systems modelled by means of PC2Rnets regarding the liveness property. Most state-ofthe-art techniques for liveness enforcing introduced in the context of FMSs are essentially based on a half-behavioural, half-structural liveness characterisation. Unfortunately, this characterisation does not apply to the more general context of PC2Rnets. This is illustrated in the chapter, while new results are provided delimiting, through necessary or sufficient conditions, the liveness problem for PC2Rnets. Additionally, new properties are presented and analysed that mark the point of disruption to the previously known characterisation, and show the roadpath for attempts to extend previous techniques and results on RAS models to the new application domain. The discussion crystallises in the proposal of a new methodological framework to enforce liveness on PC2Rmodels that makes use of the particular characteristics of the new application domain. This is accomplished through the introduction of a toolbox that is offered to the software engineer so as to correct the multithreaded software system. This toolbox relies Introduction 5 on the application of previously acquired knowledge, such as the technique of privatisation of resources, which serves as an alternative or complement to the approximation of the classical approaches of addition of virtual resources based on integer linear programming to the multithreaded software field. 4. Gadara [WLR+09] is a subclass of PC2Rfor which certain assumptions are taken with relation to the nature of the decisions which the threads can take during their execution. In Chap. 4, Gadara nets are approached from the standpoint of what has been learnt so far. In parallel, a novel proof of the structural characterisation of liveness for this kind of nets is provided. Furthermore, Gadara nets are proved to be close to another subclass of PC2Rnets rather exploited in the literature: the S4PR class. 5. Another contribution of this thesis is the statement of the computational complexity of various problems related to liveness analysis and synthesis in RASs. Accompanied by an appropriate in-depth literature review on previous work in RAS complexity, Chap. 5presents new results describing the complexity of issues related to the RAP, either directly (e.g., the problem of deciding whether a net system is live, the problem of deciding whether a marking inevitably leads to deadlock) or indirectly (e.g., the problem of detecting spurious markings). The thesis finishes with a brief summary of the conclusions of the work, as well as a discussion on the opened lines of future research. Some notational conventions Throughout this thesis, certain notational conventions have been adopted which are worth further attention. For the sake of convenience, they are grouped and explained below. On caption location and item numbering Five categories of items are numbered independently: 1. Chapters, sections, and subsections 2. Tables 3. Figures 4. Algorithms 5. Theorem-like annotations (namely: theorems, lemmas, propositions, properties, remarks and problems) 6Introduction Chapters, sections and subsections are numbered according to the usual LaTeX convention. This means that all of them get decimal numbering (except the appendixes, which get a letter) and the numbering of sections and subsections is prefixed by the chapter number or chapter and section numbers, respectively. Items in the last four categories are numbered consecutively in order of appearance within the thesis: chapter number first, then numbered sequentially within each chapter, e.g.: Table 1.1, Figure 4.2. Note that theorem-like annotations are grouped in a single category, and therefore the numbering sequence applies to all these items; e.g. Theorem 3.4 follows Proposition 3.3. The unique exception to the above general rule is in Chap. 4. Three transformation rules are defined in that chapter, which (for the sake of readability) are simply numbered 1, 2 and 3, without any chapter number prefix. The format of titles and captions of tables and figures are as consistent as possible throughout the thesis. In general, they are placed under the floating element, except in the case of large tables that span through several pages. In those cases, the caption is placed over the table top, in the first page. Table headings (if any) are repeated on the second and subsequent pages. As a exception, the caption of algorithms is always provided at the top of them. Petri net-related notational conventions The basic Petri net terminology and notation required to follow this thesis is described in Appendix A. However, a few remarks are in place at this point, since they affect many of the figures throughout the thesis. First, net markings are usually denoted in the form: [PK1 1,PK2 2, ..., PKn n], with K1, ..., Kn∈IN+. For a marking mdenoted in this way, the naturals K1, ..., Kn represent the values of the vector mcorresponding to the places P1, ..., Pnof the net, i.e., ∀i∈[1, n] : m[Pi] = Ki. If Pihas no superscript, it is assumed that Ki= 1. The rest of components of the vector mare assumed to be zero-valued. Sets are denoted following the usual curly bracket notation, e.g., {e1, e2, ..., en}. Consequently, the sets of markings (such as, e.g., livelocks) are usually denoted using curly brackets as well. For instance, {[A0,B2,C0,D1,R1],[A1,B2,C0,D1]}denotes a set containing the net markings [A0,B2,C0,D1,R1] and [A1,B2,C0,D1]. Besides, p-semiflows are often represented as marking invariants in the form: K1· m[P1] + K2·m[P2]+(...) + Kn·m[Pn] = K0, with K1, ..., Kn,K0∈IN+. In the first part of the equality, the naturals K1, ..., Knrepresent the values of the vector ycorresponding to each place P1, ..., Pnof the net, i.e., ∀i∈[1, n] : y[Pi] = Ki. The rest of components of the vector are assumed to be zero-valued. Meanwhile, K0is the result of the weighted sum of tokens in the net for a given initial marking, where y determines the weighting (in other words: K0=yT·m0). Chapter 1 Resource Allocation Systems: A facet of Discrete Event Systems Summary In the last years, the application of formal models, as Petri nets [Mur89], to the RAP has been a fruitful approach from a double perspective. First, thanks to the consolidation of an abstraction process of systems leading to models structured around the concepts of processes and resources, which can be easily translated into Petri nets. Second, thanks to the unveiling of analytical results characterising deadlock states, as well as methods to amend the problem. As a matter of fact, much of the success is based on the intensive use of structural reasoning on the Petri net model, unlike other more traditional approaches based on the state space under which real systems can hardly be considered. The process of abstraction enables the implementation of these methods to a wide range of engineering domains such as logistics, multiprocessor interconnection networks or distributed systems, although manufacturing is yet predominant. Nonetheless, the assumption of syntactic restrictions with a physical meaning is a common practice for most application domains, such as, e.g., FMSs. Almost as a corollary, a myriad of different models exist, with subtle syntactic variances between. In this chapter, a consistent and structured view is provided on the different Petri net models for RASs with sequential processes, highlighting modelling capabilities independently from the target application domains. By doing so, the shortcomings of earlier approaches brought to the multithreaded software domain are made evident. 7 81. Resource Allocation Systems: A facet of Discrete Event Systems 1.1 Introduction Economical, spatial, technical: whatever the reason, resource scarceness is a traditional scenario in diverse systems engineering disciplines. Loosely speaking, an RAS is a discrete event system in which a finite set of (scarce) resources is shared among a set of concurrent sequential processes. From a different perspective, we consider that an RAS is a view of a system from which we study the problems related to the use of shared resources. This means that in an RAS view of a system we can ignore the explicit causal relations imposed by a process to another by means of message passing, for example. Consequently, once the resource related matters are solved, we can proceed with the next phase of the analysis/design of the system in which other facets of it are incorporated. This description or view has been successfully applied on a broad family of systems which range in disciplines such as manufacturing, distributed computing, operations research, networking or logistics. Thanks to a prior process of abstraction which is inherent in the discipline, RASs can be conceptualised under system models conceived around two distinct entities: processes and resources. Consequently, syntax restrictions on formal models for RASs can be roughly classified according to two basic criteria [RLF97]: first, to the structure (control flow) of the concurrent processes; second, to the way the resources are used by these processes. Beyond this coarse-grained categorisation, the variety of domain-specific physical constraints has led to a proliferation of works which study subtly different abstract models for RASs with strong structural restrictions. Most often these feature an expressive power well adapted to specific application domains, while powerful solutions are known for them. From this perspective, and taking into account some usual physical constraints in the context of flexible manufacturing systems (sequential processes, non-consumable resources, etc.), the success of some Petri net-based methodologies for studying the deadlock problem seems well justified. Generally, the aforementioned abstract models are used to study the RAP: the procedure in serving the processes requirements for resources, according to their own resource usage policy, while accomplishing a certain goal. In fact, such a generic definition encompasses different problems from a qualitative or quantitative standpoint. In quantitative terms, the concept relates to the ability of optimising a system performance function [KS89]. In qualitative terms, it is widely associated to satisfying successfully the requests for resources made by the processes, ensuring that no process ever falls in a deadlock [LT79]: the focus of this thesis. Although other models of concurrency have also been considered [FMMT97], Petri nets [Mur89] have arguably taken a leading role in the family of formal models used for dealing with the RAP [ECM95,ER04]. One of the strengths of this approach is the smooth mapping between the main entities of RASs and the basic elements of Petri nets. 1.2. The role of abstraction 9 This fact is well recognised in the domain of FMSs, where Petri net models for RASs have widely succeeded since the seminal work on the matter was introduced [ECM95]. This is based upon two solid pillars: 1) the definition of a rich syntax from a physical point of view, which enables the natural expression of a wide disparity of plant configurations; and 2) the contribution of sound scientific results which let us characterise deadlocks from the model structure, as well as provide a well-defined methodology to automatically correct them in the real system. Section 1.2 focuses on RASs from the point of view of the key role played by the process of abstraction in obtaining tractable models for different application domains. In that sense, common elements in the abstraction of processes and resources are categorised from a systemic point of view. This is a relatively unexplored approach to the problem, since most works start from the specific study of an application domain. From this general framework, the different state-of-the-art Petri nets classes are categorised in Sect. 1.3. Finally, in Sect. 1.4, the class of S4PR nets is introduced as a starting paradigm of the methodology. To this aim, a simple example from the field of FMSs is presented. 1.2 The role of abstraction As introduced above, the methodological approach discussed in this thesis is based primarily on obtaining manageable formal models from the observation of real-world systems. To this end, we must discard those irrelevant details for the property to be studied (in this case, for the emergence of deadlocks due to an inappropriate resource allocation sequence), while preserving those relevant aspects. Such process is known as the process of abstraction [GW92]. In this sense, an RAS constitutes a facet of a real world system [Zei84], i.e., a particular, restricted, non-exclusive view of it. For instance, in the context of multithreaded software, deadlocks can occur not only due to some resource allocation order, but also to message passing between different threads. Within the scope of this thesis, an RAS view of such systems will be addressed in which details of the message passing are ignored. Therefore, this kind of deadlocks is not reflected in the resulting models. The philosophy of the methodology proposed in this thesis consists in, as discussed in Chap. 2, first resolving the deadlock problems through an RAS vision, moving later to address the deadlock problems caused by other communication/synchronisation paradigms. In short, an RAS is just the intellectual product resulting from the application of a process of abstraction on the system studied. The importance of the abstraction process must be emphasised because in fact it implies a particular methodology for the design of complex systems. In effect, a system is not a pure RAS in general because of processes that impose causality relations to other processes in the system. Consequently, when we retain processes 10 1. Resource Allocation Systems: A facet of Discrete Event Systems and resources ignoring the rest of relations in the system we advocate for analysing and correcting the problems associated to the use of resources. Once this goal is accomplished, the designer can concentrate in other systemic problems, such as those related to performance, scheduling or others. In fact, this is the design flow assumed in this thesis. This approach to system design is the deep reason to promote structural methods to correct or fix problems. Indeed, such methods can survive to further steps in the design concerning performance or optimisation. Through the process of abstraction we obtain higher-level items such as resources and processes, and relations between them. The concept of what is and is not a process (or resource) is dependent on the application domain to be studied. In fact, although in this section we discuss the process of abstraction as an entity which is abstract in itself, in practice it makes no sense to speak of a single process of abstraction. On the contrary, it would be more reasonable to speak of a family of them, each one closely linked to an application domain and even sometimes to a particular case study. In this regard, it may suffice to exemplify the last observation through a particularity. In the process of abstraction for the study of the RAP, the fact that an element of the real system is considered a resource often makes practical sense only if it intervenes, or may intervene, in situations of deadlock. For this it is necessary (though not sufficient) that the resource is held at some time while waiting for the allocation of a different resource so as that the system (or part thereof) can progress: a property known in the realm of operating systems as “hold & wait” [CES71]. Otherwise, for the sake of conciseness and manageability of the resulting RAS model, it is unnecessary to consider the item as a resource in it. On the other hand, given that the steps of a process that are relevant to the RAP are somehow related to the set of resources involved, the aforementioned issue can also affect the size or structure of the processes (understood as abstract entities). Or, even, it might involve their disappearance from the model if no other resource interacts with them. In short, the concept of process and resource is heavily dependent not only on the application domain, but also on the particular conditions of the problem to be studied. Given the foregoing, it is still possible to sketch an outline of the main steps that constitute the process of abstraction to obtain an RAS. Broadly speaking, the common features in the abstraction of systems of very diverse nature could be catalogued according to the following road map: 1. Resource identification. The Collins English Dictionary defines a resource as ‘a supply or source of aid or support; something resorted to in time of need’ or ‘a means of doing something’ [Col11]. A first important consideration is that the nature of this medium can be logical, and as such, there is no need for a visibly located physical embodiment of an element to be considered as a resource from an RAS point of view. A simple example of this in the field of manufacturing 1.2. The role of abstraction 11 systems is the consideration of storage space as a system resource. Indeed, the lack of storage space for a part in transit in the manufacturing system can be a cause of circular waits in the system and therefore of deadlocks. It is also possible to consider a group of physically dispersed elements as a single resource for the sake of the study of the RAP if all of them are always used in unison under the same circumstances. The possibilities are very diverse under the interpretation of various application domains. Another relevant consideration concerns the way a resource is seen with respect to its interaction with the rest of the system. From an RAS point of view, resources are passive elements in the sense that their behavior can be summarised in two states (allocated or free) and that the change from one to another state can be fully explained from the evolution of the rest of the system. In fact, the latter behaviour should apply for all resources considered in the system. Considering the above, two types of high-level operations can be identified: assignment operations, which wait until the resource is free and switch its status to assigned, and release operations, which switch the resource status from allocated to free. It is important to note that the assignment operation thus conceived is a blocking operation (i.e., if the resource is not free, then the system, or that part of the system, wait for it to be). Therefore, a parallel identification of operations that interact with the resources is important in order to decide what should be considered a resource in our high-level abstraction. Another fundamental aspect to consider is whether the resources can be grouped into sets of resources that can be used interchangeably at all times. In that sense, returning to the previous example in the context of manufacturing systems, we could quantify the storage space in a given buffer content, where a single resource would be considered the gap that a piece would fill by being placed at the buffer. Obviously, all gaps should stand on equal footing for all system operations, so that any free resource of the set can be chosen whenever one of these is required. When we find such an scheme, we can reach a higher level of abstraction that simplifies the vision of the system: the existence of resource types. 2. Process identification. The Collins English Dictionary defines a process as ‘a series of actions that produce a change or development’ or ‘a method of doing or producing something’ [Col11]. Unlike resources, processes are the active elements of the system from an RAS point of view. Processes are patterns of behavior of the system, potentially repetitive and often sequential, that are observable from a local perspective. Note that the condition of locality here does not refer to a physically contiguous location for the operations that compose it, but to the existence of a certain order relation between them or between groups of them, so that their repetition is closely linked. Or, more appropriately, to 12 1. Resource Allocation Systems: A facet of Discrete Event Systems the possibility of discerning a control flow that relates them logically. At this point, one may notice a new category of significant operations beyond those of resource allocation and release. These operations are those that alter the control flow of a particular process, either breaking or restoring their sequentiality (e.g., job splitting/merging operations in the context of FMSs) or by establishing alternative execution paths or reunifying them (e.g., chain branching). Such operations can also be coupled with those above, so that the alteration of the control flow is subject to the allocation of certain resource(s). In line with this last point, it should be noted that, from the point of view of the processes, the allocation and release operations may require different resource types, or multiple instances of the same type, simultaneously. This is another question that must be evaluated in order to characterise the process of abstraction of the system and finally determine the type of model required to properly study the problem. Finally, processes following the same behavioural pattern may concur in the system. Similar to the approach undertaken with resources, this observation leads to the introduction of a higher level abstraction that can result in more compact models: the existence of process types that may or may not have a certain capacity (i.e., maximum number of concurrent instances). 3. Modular construction of the model. A modular abstraction, and thus ending up with a modular model, is natural in such abstractions. This is because RASs consist of multiple concurrent active entities that, if they had enough resources to progress, could ignore each other. As resources are limited, the construction is done by overlapping entities via use of shared resources. Essentially, the modelling stage consists in the embodiment of the product of the abstraction process through a formal language. Thus, strictly speaking, modelling cannot be considered part of the process of abstraction. Nonetheless, it is still a process closely linked to the process of abstraction, to the extent that the latter is often consciously or unconsciously influenced by the type of target model. Note that in other abstractions modularity is not evident as a constructive principle, but that is not the case of RASs. In that sense, the choice of a formal model with restricted expressiveness can derail the study of the desired property. The versatility and modularity of Petri nets, however, seems to provide a natural setting which is suitable for the expression of the various entities involved in an RAS in due complexity. This issue is revisited in Sect. 1.3. In the case of Petri nets, the modeling methodology is based on three steps: characterisation of the processes, incorporation of the resources, and construc- 1.3. The resource allocation problem through Petri net models 19 belongs to some p-semiflow (and resources are used conservatively) then the system is structurally bounded. •Ordinary resource subnets. This property essentially refers to the simplicity of the resource request/release operations. If such operations allow requesting/releasing multiple instances of the same resource type, then the corresponding arcs in the resource subnets are weighted (i.e., some subnets are nonordinary). In general, the more complex the allocation operations, the more difficult the model is to analyse. •Binary resource p-semiflows. Stricter than the preceding one, this model restriction is applicable when processes never request several instances of the same resource type, neither simultaneously nor in an successive requests. Instead, an allocated resource must be released prior to any other allocation request of a resource of the same type. •Orthogonal resource p-semiflows. The orthogonality of the resource p-semiflows implies that a process can only simultaneously use resources of a single resource type. Prior to requesting resources from a different resource type, it must release all its allocated resources. This property often comes coupled with the preceding one [ECM95,EGVC98]. When both restrictions apply, at most one resource can be allocated to each process at a given state of execution. •Resource-independent internal conflicts. This property holds when each conflict belonging to a single process path is fully non-deterministic with respect to the allocation state of resources. In other words, resource allocation operations are conceived as strictly blocking operations: whenever a process requests some resources, it cannot advance in whichever other way until that precise request is granted (and no other set of available resources can serve as an alternative). •Resource lending. In some application domains, it may be necessary to consider the fact that a resource can be created by some process, shared with other processes, and finally destroyed by the same process that created it. This is done in such a way that there still exists an invariant relation that ensures that these new resource is serially reusable by the concurrent processes. Notice that under certain circumstances (namely, when the process subnets are open) this invariant relation may no longer be captured by the concept of resource p-semiflow, and certain specific p-flows are used instead. All of this is further discussed in Chap. 2from the perspective of the modelling of multithreaded software systems. This phenomenon is labelled as resource lending, since some resources are somewhat lent by some ‘server’ processes to other ‘client’ processes. 20 1. Resource Allocation Systems: A facet of Discrete Event Systems •First allocated, first released. This property establishes a link between the allocation operations and the release operations within every single process path, in such a way that resources are released in the same order as they were allocated. In many cases (e.g., as that of multiprocessor interconnection networks) this is a natural restriction imposed by the application domain, as discussed in Subsection 1.3.3. 1.3.2 Petri net models for RASs Despite the existence of other works based on formal models [FMMT97], Petri nets have proven to be an especially useful tool for the modelling, analysis and synthesis of RASs with serially reusable resources [LT79,ECM95,GV99,JX01,PR01,ETGVC02, Tri03,Col03,ER04,JXC04,TGVCE05,LDZ06]. With respect to the structure of the concurrent processes, most of the current work focuses on Sequential RASs, as opposed to Non-Sequential RASs, in which assembly and disassembly (fork / join) operations are allowed within the processes. However, some studies have attempted to approach Non-Sequential RASs using Petri nets as modelling paradigm. Classes such as Non-Sequential Resource Allocation Process (NS-RAP) [ER04], Extended Resource Control Net (ERCN) merged nets [XJ99], ERCN*merged nets [JXC04] or Process Nets with Resources (PNR) nets [JXP02] extend the capabilities of conventional models beyond Sequential RASs by way of lot splitting or merging operations. Unfortunately, finding effective solutions for these systems is, in general, much more complicated [XJ99]. As for Sequential RASs, which are the subject of study in this PhD thesis, it is worth mentioning the disparity of Petri net models that have emerged successively, often extending previous results and thus extending the subclass of systems that can be modelled and studied. The Cooperating Sequential Systems (CSS) class is one of the first classes designed to study the RAP in Sequential RASs [LT79]. In CSS, there is only one type of process, i.e., all processes share identical structure of stages or steps to execute. These processes may compete for multiple resource types, with possibly multiple instances of each type. In more recent works on Sequential RASs, the existence of multiple process types is supported, usually allowing different routes or alternative execution plans. In some of these models, however, the execution plan of a process is chosen at the launch of its execution, and remains fixed throughout the course of it [FMMT97]. Other works overcome this limitation, supporting routing decisions at runtime. In particular, so it is with the seminal S3PR class [ECM95]. However, the processes of an S3PR net can reserve at most one single resource in each stage or execution step. Also of note is the existence of subclasses of S3PR (like Linear S3PR (L-S3PR) nets [EGVC98]) with interesting structural properties. The restriction on the resources usage per process is overcome by the S4PR 1.3. The resource allocation problem through Petri net models 21 class [Tri03,TGVCE05], also named S3PGR2[PR01], which is a superclass of S3PR. This class allows runtime routing decisions, as well as the simultaneous reservation of multiple resources of different types by a single process. These resources can be released in an arbitrary order. Systems of this type are occasionally named DisjunctiveConjunctive RASs [RLF97]. Particularly, the S4PR class has received special attention because it can deal with a fairly general class of Sequential RASs, and efficient characterisations exist for deadlock situations [Tri03]. Although most of these works emphasise the application in FMS, the use of a purely systemic approximation allows to apply these models, as well as the techniques developed for analysis and synthesis [ETGVC02,TGVCE05], to very different application domains. Another interesting subclass of S4PR is that of S4PR with Ordered Allocation and Release of the Resources (SOAR2) [Rov11]. In this case, the resources are managed in a “first allocated, first released” basis by the processes, and the model structure is restricted to adhere to this particularity. This characteristic is inherent to some application domains such as wormhole communication in multiprocessor interconnection networks. This is further discussed in Subsection 1.3.3. At present, the most general class of Petri nets for Sequential RASs is the S*PR class [ETGVC02], in which processes are ordinary state machines with internal cycles. However, deadlocks in S*PR net models are not fully comprehended from a structural perspective. A more detailed study on the relationships between the different kinds of nets was published in a previous work [Col03]. It should be noted that for all the above classes except for the S*PR class, there exist liveness characterisations based on the absence of certain types of partially unmarked siphons. The structural nature of such characterisations opens a door to the efficient detection and correction of deadlocks, by implementing controllers (usually by adding new places) that restrict the behaviour of the net, preventing the reach of undesirable markings. There exist, however, other studies that try to address the problem of processes with internal cycles, always starting from certain restrictions on the approach of the S*PR class regarding the use of resources within those cycles [JX01,JXC04,LDZ06]. One of these Petri net subclasses is that of Gadara [WLR+09]. Gadara nets are presented as a model for studying the RAP in multithreaded software systems sharing a set of binary locks. Gadara nets therefore feature binary resources and internal cycles are allowed within the structure of the processes. However, all conflicts in the process paths of a Gadara net are resource-independent. Unfortunately, it is not hard to find real-world systems in which the above restriction does not apply. This deficiency is addressed along this thesis in the framework of the study and exploitation of the RAP in the context of multithreaded software. In particular, Chap. 4carefully approaches Gadara nets from a critical position. Finally, the class of System of Processes Quarrelling over Resources (SPQR) [LGC06] notably diverges from the previous approaches in an attempt to 22 1. Resource Allocation Systems: A facet of Discrete Event Systems generalise the systems considered in the traditional modelling of FMSs from an RAS perspective. This generalisation is essentially driven in two directions. First, the process subnets are open systems. Second, resource lending is allowed. SPQR nets will be thoroughly studied in Chap. 2. Table 1.1 relates the Petri net classes mentioned above with the model properties presented in Subsection 1.3.1. The table draws a more complete picture of the relationships between them from an essentially syntactic viewpoint. 1.3.3 Deployment of the RAS vision in different domains Having reviewed the steps which are necessary to realise the process of abstraction, in this section we focus on the observation of some application domains in which the RAS approach has led to relevant results. In this course of action, we identify the basic functional entities which are abstracted in the process. Consequently, those aspects which were previously introduced from a conceptual perspective are here materialised. The RAP in Flexible Manufacturing Systems The problem of deadlocks due to an inappropriate resource allocation sequence is very well-known in the field of FMSs, where the RAS approach has a long, successful road [Col03]. In this area, an RAS would be a view of a manufacturing cell where resources are often machines or tools that are used to achieve the manufacturing process. Such tools can be fixed processing elements such as workstations, as well as transport mechanisms such as robotic arms or conveyor belts. As noted above, it is also possible to consider the space in containers or pallets as system resources used to hold parts in the process. Figure 1.1 depicts a production cell with two robotic arms and three workstations, as well as conveyor belts for the input and output of material. On the other hand, the processes of the RAS would be the parts being processed in the system. Each of these parts follows a prefixed production plan which is divided into different stages where operations are executed. These operations can be classified into different types closely related to the various types of resources mentioned above (transformations, handling, storage, etc.). Such production plans would be our “process types”. For example, a process type would be the production plan for the cell of Fig. 1.1 in which, first, parts from I1 are taken to M1 through R1. Second, the arm moves them, when processed, from M1 to M2. And finally, after the processing in M2 is completed, R1 moves them to O1 so as to leave the cell. Parts following different production plans but sharing a nonempty set of resources can concur in the system, which may be a source of deadlocks. At this point, it is important to discern whether parts can be assembled and disassembled in the system. Assembly/dissassembly operations can have a dramatic impact 1.3. The resource allocation problem through Petri net models 23 CSS [LT79] L-S3PR [EGVC98] S3PR [ECM95] SOAR2[Rov11] Gadara [WLR+09] S4PR [TGVCE05] S*PR [ETGVC02] PNR-nets [JXP02] ERCN*-merged [JXC04] NS-RAP [ER04] SPQR [LGC06] Properties of the whole system Unique process subnet X×××××××××× Closed process subnets XXXXXXXXXX× Binary resources ×××X X ×××××× Structural properties of the processes Reproducibility of t-semiflows XXXXXXXXX×X Consistency XXXXXXXXXXX Equivalence of t-semiflows XXXX×X×X××X Process termination XXXXXXXXX×X Process liveness XXXXXXXXX×X No internal decisions XX××××××××× Process sequentiality XXXXXXX×××X Properties about the use of resources Conservativeness XXXXXXXXXXX Ordinary resource subnets ×XXXX××X X × × Binary resource p-semiflows ×XXXX×××××× Orthogonal resource p-semiflows ×XX×××××××× Resource-independent conflicts XX× × X×××××× No resource lending XXXXXXXXXX× First allocated, first released ×XXX××××××× Table 1.1: Modelling capabilities of some well-known Petri net classes for RASs 24 1. Resource Allocation Systems: A facet of Discrete Event Systems R1 R2 M1 M2 M3 I1 I2 O1 Figure 1.1: Layout of a manufacturing cell on the complexity of the analysis of the problem, as discussed in Subsection 1.3.2. Furthermore, it is important to note that in such systems the production plans often have a very specific structure, in which all operations, or large groups of them, are fully or partially ordered. Besides, it is unusual to find internal cycles, as recirculating circuits; or if any, there are usually few of them, having no major ramifications and being well located. In general, the predominant element regarding changes in the process flow is the routing of parts into different production branches. Again, this peculiar type of structure has been well exploited by the application of formal methods (and particularly Petri nets) to the study of the RAP. Most of the Petri net models presented in Subsection 1.3.2 have been conceived with FMSs in mind as the target application domain. From a modelling point of view, the problem of integrating assembly/dissassembly operations has been approached in several works. Classes such as NS-RAP [ER04], ERCN merged nets [XJ99], ERCN*merged nets [JXC04] or PNR nets [JXP02] were proposed in the context of approaching the RAP in FMSs. However, structural liveness enforcing approaches can be computationally demanding in this scenario, as evidenced for augmented marked graphs [XJ99]. An insight on the computational complexity of such approaches on the Sequential RAS context is driven in Chapt. 5. In most recent works in the context of Sequential RAS, different process types with multiple concurrent instances are allowed, often allowing on-line routing decisions into different production branches. In particular, such kind of FMSs are dealt with the seminal S3PR class [ECM95]. However, processes in a S3PR net can use at most a single resource unit at a given state. The same applies for its subclass L-S3PR [EGVC98], also conceived to approach certain FMSs. Although more restric- 1.3. The resource allocation problem through Petri net models 25 N1 N2 N4 N5 N3 N6 C A0 C B0 C H0 C A1 C B1 C H1 C A2 C B2 C H2 C A5 C B5 C A3 C B3 C H3 C A4 C B4 C H3 Figure 1.2: Layout of a multiprocessor interconnection network with an unidirectional ring topology tive, L-S3PR nets are very interesting from an analytic point of view. The mentioned restriction over resources usage is eliminated by the (more general) S4PR class [Tri03,TGVCE05]. This allows processes to simultaneously reserve several resources belonging to distinct types. Nowadays, this is the most general class that allows modeling FMSs while maintaining a complete correction methodology based on efficient structural analysis and synthesis techniques. However, a few more general net classes (SPQR,S*PR) have been proposed in the realm of approaching the RAP in FMSs. This PhD thesis attempts to push the boundaries of those structural techniques into this essentially unexplored ground. The RAP in multiprocessor interconnection networks In recent times, novel results have seen the light in the development of a methodology for the design of deadlock-free minimal adaptive routing algorithms for multicomputer interconnection networks from an RAS perspective [Rov11]. From this point of view, an RAS within the multicomputer interconnection network would be a potential view of it with messages in transit between nodes. Here, the resources are the channels available for communication between nodes, be those physical or virtual. Figure 1.2 shows a network of this type with six nodes, an unidirectional ring interconnection topology, and a variable number of channels between the interconnected nodes. In the particular case of routing in communication networks using wormhole flow control [DS86,Dua95], deadlocks can occur by the emergence of circular waits due to the reservation of channels for simultaneous communication of different messages, each of which is composed of a row of elementary flow units called flits. Such situations are difficult to detect when the routing algorithm is adaptive, i.e., routes are non-preset but dynamic depending on the traffic. 26 1. Resource Allocation Systems: A facet of Discrete Event Systems In networks with wormhole flow control, flits travel in a row through the interconnection network by establishing a virtual path. The first of these flits is called head and reserves the channels through which, in turn, the rest of flits will be orderly sent. The last of those flits, called tail, releases the channels reserved by the head, which are then made available for sending flits of other messages. In this context, a process is the routing of a message. Each process consists of the various states that a message undergoes from source to destination through the interconnection network. Therefore, the state of a process in networks with wormhole flow control is determined by the location of the head and tail flits, as well as by the sequence of channels that are still reserved for the transmission of the message, and that the queue must release. Unlike manufacturing systems, we can see that the state of a process does not have a clear physical location (i.e., a part located on a stage of the production line using some resources) but is somehow scattered in space. In general terms, the structure of a process is determined by the network topology, the routing algorithm and the flow control model. A particular feature of the networks with wormhole flow control stems from the fact that the reservation and release of channels (resources) by the processes is conducted in a unitary and sequentially ordered way following a policy that might be called ‘first allocated, first released’. In the case of static routing, the structure of the processes shall also be linear, which greatly facilitates determining whether the system is deadlock-free. The use of adaptive routing algorithms (i.e., dynamic) marks the possibility of finding alternative paths (decisions) and merges in the structure of the processes. Furthermore, the minimality of the adaptive routing algorithm guarantees the absence of internal cycles in the structure of the processes. Assuming unicast communications, the types of processes would be determined by the various destinations. Approaching the problem of minimal adaptive routing in multiprocessor interconnection networks from the perspective of RASs is a novel initiative. As such, the corpus of knowledge is essentially condensed throughout a single PhD thesis [Rov11] and external contributions in this area are yet to emerge. That thesis tackles the aforementioned problem in interconnection networks with wormhole flow control providing a particular subclass of S4PR to model and analyse this kind of systems: the SOAR2class. The definition of this class takes advantage of the peculiar physical constraints of the domain. Despite this limitations, the groundbreaking synthesis approach developed throughout this thesis is relevant for the study of the RAP in the multithreaded software domain. In essence, there exists a disruption here with the classical synthesis methods based on the addition of monitor places that restrict the system behaviour. This disruption came somewhat forced by the need for a truly, unavoidable ‘distributed’ control approach that can be obviated in the context of FMS, but which is much convenient, even sometimes indispensable, in the concurrent software domain. We delve into this issue throughout Chap. 3. 1.3. The resource allocation problem through Petri net models 27 Figure 1.3: Example of deadlock in a tow type AGV transportation system The RAP in transportation systems Viewed from an RAS perspective, there are significant parallels between Automated Guided Vehicle (AGV) transportation systems and multicomputer interconnection networks [Rov11]. In particular, in the case of tow type AGVs applied for in-plant material transport, strong resemblances can be traced between deadlocks caused by the blocking of path segments and those emerging in interconnection networks with wormhole flow control. Figure 1.3 illustrates a possible deadlock of this nature. Those commonplaces have been studied in depth in order to establish a design methodology of deadlock-free minimal adaptive routing algorithms for such systems [Rov11]. In this case, the resources are the segments visited by the AGV. These segments are occupied by the AGV as soon as the tow tractor (the head) enters in them (that includes the decision points that delimit the segment) and are not released until the last of the carts (tail) leaves. In turn, a process is the transport of goods from a source point (location / station) to a destination point. Following this scheme, it is easy to understand the aforementioned parallel with multicomputer interconnection networks with wormhole 28 1. Resource Allocation Systems: A facet of Discrete Event Systems flow control, again being the structure of the processes dependent on the plant topology and the routing algorithm proposed for the AGVs. The observation previously stated on the synthesis techniques applicable to multiprocessor interconnection networks can be fully extrapolated to the context of the development of deadlock-free minimal adaptive routing algorithms in tow type AGV transportation systems. This parallelism is examined throughout the said PhD thesis, and the results of this work will be exploited and extended in Chap. 3. It should also be mentioned the existence of some other works that address the modeling and analysis from a RAS point of for other types of AGV transportation systems, although the techniques of analysis and correction, when presented, do not always address the problem from a structural standpoint [Rev00,Fan02,WZ05]. The RAP in multithreaded software systems Although there exist a significant number of works that approach the modelling of concurrent programming through Petri nets [IA09], only a handful of them approach multithreaded software from the perspective of RASs [LGC06,WLR+09,Wan09, LGC12], often either with severe limitations in the class of software systems which are subject of study or lacking a complete methodology to correct the liveness problems. This PhD thesis tries to fill this gap in the literature. To this end, the abstraction and modelling of this kind of systems is tackled in Chapter 2. On the other hand, the limitations of the Gadara project, an alternate approach in the same vein [Wan09], are studied in depth in Chapter 4. 1.4 The class of S4PR net systems In order to illustrate all the ideas previously presented about the different classes of Petri nets that are currently used to model RASs we recall here the definition of S4PR. This class is fundamental because it represents the largest class for which the analysis and synthesis results allow to dispose a complete methodology to construct good RASs. We have syntactic constraints but they are general enough to cover many real applications as those previously presented. Historically, the S4PR class appeared as a generalisation of the seminal S3PR class which was proposed to extend the existing techniques to a more general category of RASs. In this generalisation, the structure of the processes is left intact, and the novelty lies in the fact that several resources can be simultaneously allocated to a single process. Although, S4PR nets were originally proposed to deal with FMSs, they can be applied to other domains, as discussed in Sect. 1.3. S4PR nets are modular models composed of state machines with no internal cycles plus shared resources. One of the most interesting features of this kind of models is 2.2. The RAS view of a software application 35 is a circular table surrounded by five chairs, each belonging to one philosopher. A microwave oven is also available. In the centre of the table there is a large bowl of spaghetti which is frequently refilled (so it cannot be emptied), and the table is laid with five forks. On feeling hungry, a philosopher enters the dining room, sits in his own chair, and picks up the fork on the left of his place. Then he touches the bowl to feel its temperature. If he feels the spaghetti got too cold, he leaves his fork and takes the bowl to the microwave. Once it is warm enough, he comes back to the table, sits on his chair and leaves the bowl on the table after recovering his left fork. Unfortunately, the spaghetti is so tangled that he needs to pick up and use the fork on his right as well. If he can do this before the bowl gets cold again, he serves himself and starts eating. When he has finished, he puts down both forks and leaves the room.” According to the classic RAS nomenclature, each philosopher is a sequential process, and the five forks plus the bowl are serially reusable resources which are shared among the five processes. From a software perspective, each philosopher can be a process or a thread executed concurrently. Algorithm 2.1 introduces the code for each philosopher. Notationally, the acquisition / release of resources is modelled by way of the wait() /signal() atomic operations, respectively. Both of them have been generalised for the acquisition of multiple resources (separated by commas, inside the parentheses, when invoking the operation). Finally, trywait() models a non-blocking wait operation. If every resource is available at the time trywait() is invoked, then it acquires them and returns TRUE. Otherwise, trywait() will return FALSE without acquiring any resource. For the sake of simplicity, it is assumed that the conditions with two or more literals are also evaluated atomically. Figure 2.1 depicts the net for Algorithm 2.1, with i= 1, after abstracting the relevant information from an RAS perspective. Figure 2.2 renders the composition of the five philosopher nets via fusion of the common shared resources. Note that if the dashed arcs from Fig. 2.2 are removed, then we can see five disjoint strongly connected state machines plus six isolated places. Each state machine represents the control flow for a philosopher. Every state machine is composed of seven states (places). Tokens in a state machine represent concurrent processes/threads which share the same control flow. At the initial state, every philosopher is thinking (outside the room), i.e. the unique token in each machine is located at the so-called idle place. In general, the idle place can be seen as a mechanism which limits the number of concurrent active threads. Here, at most one philosopher of type ican be inside the room, for each i∈ {1, ..., 5}. The six isolated places are called resource places. A resource place represents a resource type, and the number of tokens in it represents the quantity of free instances of that resource type. In this case, every resource place is monomarked. Thus, at 36 2. The resource allocation problem in software applications Algorithm 2.1 - Code for Philosopher i (where i∈ {1,2,3,4,5}) T3 FORK1 FORK2 BOWL A4 A3 T4 T5 T1 T6 T7 A6 T8 A0 A1 A5 A2 T2 Figure 2.1: Philosopher 1 var fork: array [1..5] of semaphores; // shared resources bowl: semaphore; // shared resource begin do while (1) THINK; Enter the room; (T1) wait(fork[i]); (T6) do while (not(z }| { trywait(bowl, fork[i mod 5 +1])) or the spaghetti is cold) (T2) if (trywait(bowl) and the spaghetti is cold) then (T3) signal(fork[i]); Go to the microwave; Heat up spaghetti; Go back to table; (T4) wait(fork[i]); (T5) signal(bowl); end if; loop; Serve spaghetti; (T7) signal(bowl); EAT; (T8) signal(fork[i], fork[i mod 5 +1]); Leave the room; loop; the initial state there is one fork of type i, for every i∈ {1, ..., 5}, plus one bowl of spaghetti (modelled by the resource place at the centre of the figure). Finally, the dashed arcs represent the acquisition or release of resources by the active threads when they change their execution state. Every time a transition fires, the total amount of resources available is altered. Please note, however, that moving one isolated token of a state machine (by firing its transitions) until the token reaches back the idle state, leaves the resource place markings unaltered. Thus, the resource usage is conservative. At this point, some capabilities that an RAS model should have so as to support the modelling of concurrent programs are discussed. State machines without internal cycles are rather versatile for modelling sequential processes in the context of FMSs. In FMSs, the process plans containing internal loops 2.2. The RAS view of a software application 37 Fork 2 Fork 1 Fork 3 Fork 4 Fork 5 Figure 2.2: The dining philosophers are thinking. Arcs from/to PRare dashed for clarity exist. Nevertheless, the number of iterations is usually constant and independent of the raw parts to be processed. Consequently, from the point of view of modelling, loops are unrolled and models without internal loops are generated. The success of the S3PR and S4PR classes, in which every circuit in the state machines traverses the idle place, proves the claimed versatility of the approach. Nevertheless, this is clearly too constraining even for very simple software systems. Considering B¨ohm and Jacopini’s theorem [Har80], however, it can be assumed that every non-structured sequential program can be refactored into a structured one using while-do loops. In this case, many loops cannot be unrolled, because the number 38 2. The resource allocation problem in software applications of iterations depends on the value of some data to be processed during the process runtime. Meanwhile, calls to procedures and functions can be substituted by inlining techniques. Let us also remind that fork/join operations can also be unfolded into isolated concurrent sequential processes, as some works evidence [ER04]. As a result, process models can be restricted to state machines in which decisions and iterations (in the form of while-do loops) are supported, but not necessarily every kind of unstructured branch. Another significant difference between FMSs and software systems from an RAS perspective is that resources in the latter are not necessarily physical (e.g., a file) but can also be logical (e.g., a semaphore). This has strong implications in the degree of freedom in allocating those resources: this issue will be further inspected later. In this domain, a resource is an object that is shared among concurrent processes/threads and must be used in mutual exclusion. Since the number of resources is limited, the processes compete for the resource and use it in a non-preemptive way. This particular allocation scheme can be imposed by the resource access primitives, which may be blocking. Otherwise, the resource can be protected by a binary semaphore/mutex/lock (if there is only one instance of that resource type) or by a counting semaphore (multiple instances). Note that this kind of resources can be of varied nature (e.g., shared memory locations, storage space, database table rows) but the required synchronisation scheme is inherently similar. On the other hand, it is well-known that semaphores used in that context can also be seen as non-preemptive resources which are used in a conservative way. For example, a counting semaphore that limits the number of connections to a database can be interpreted in that way from an RAS point of view. Here processes wait for the semaphore when attempting to establish a database connection, and release it when they decide to close the aforementioned connection. However, semaphores also perform a relevant role as an interprocess signalling facility, which can also be a source of deadlocks. In this chapter, the goal is the study of the RAP, so this mode of use is out of scope. Instead, it is proposed to fix deadlock problems due to resource allocation issues firstly, and later apply other techniques for amending those due to message passing. Due to their versatility, semaphore primitives are interesting for studying how resources can be allocated by a process/thread. For instance, XSI semaphores (also known as System V semaphores) have a multiple wait primitive (semop with sem op<0). An example of multiple resource allocation appears in Algorithm 2.1. Besides, an XSI semaphore can be decremented atomically in more than one unit. Both POSIX semaphores (through sem trywait) and XSI semaphores (through semop with sem op<0 and sem flag=IPC NOWAIT) have a non-blocking wait primitive. Again, Algorithm 2.1 could serve as an example. Finally, XSI semaphores also feature inhibition 2.2. The RAS view of a software application 39 mechanisms (through semop with sem op=0), i.e. processes can wait for a zero value of the semaphore. All these implementations of the semaphore API use a waiting queue of pending processes for completing wait operations on 0-valued semaphores. In this thesis, this queue is ignored in order to consider the inherent non-determinism of the operating system scheduler when imposing an ordering to the processes attempting to enter in the queue of the semaphore. As suggested earlier, the fact that resources in software engineering do not always have a physical counterpart is a peculiar characteristic with consequences. In this context, processes do not only consume resources but also can create them. A process will destroy the newly created resources before its termination. For instance, a process can create a shared memory variable (or a service!) which can be allocated to other processes/threads. Hence the resource allocation scheme is no longer first-acquirelater-release, but it can be the other way round too. Still, all the resources are used conservatively by the processes (either by a create-destroy sequence or by a waitrelease sequence). As a side effect, and perhaps counter-intuitively, there may not be free resources during the system startup (as they still must be created), yet the system is live. Nevertheless, the kind of software systems to be considered in this study will be limited. The following typical features that can appear in a program will not be considered for the moment: •Dynamic creation of new types of functionality implemented throughout threads based on functions which were not present in the initial state. •Function recursion. •Reentrant routines outside the caller’s address space. Coroutines. •Software or hardware interrupts. •Signalling facilities. Besides, internal choices of the processes determined by the value of a datadependent expression (i.e., not dependent on semaphores) will be represented as nondeterministic choices (i.e., free choices). Summing up, for successfully modelling RASs in the context of software engineering, a Petri net model should at least fulfil the following requirements: 1. The control flow of the processes should be represented by state machines with support for decisions (if-then-else blocks) and nested internal cycles (while-do blocks). 2. There can be several resource types and multiple instances of each one. 40 2. The resource allocation problem in software applications 3. State machines can have multiple tokens (representing concurrent threads) executing the same function. 4. Processes/threads use resources in a conservative way. 5. Acquisition/release arcs can have non-ordinary weights (e.g., a semaphore value can be atomically incremented/decremented in more than one unit). 6. Atomic multiple acquisition/release operations must be allowed. 7. Processes can have decisions dependent of the allocation state of resources (due to the non-blocking wait primitives, as in Fig. 2.2). 8. Processes can lend resources. As a side effect, there could exist processes that depend on resources which must be created/lent by other processes With these characteristics in mind, the next section defines a class of Petri nets to cope with these requirements. 2.3 The PC2R class 2.3.1 Functional entities. Representation In this section, a new Petri net class is presented: the class of Processes Competing for Conservative Resources (PC2R). This class fulfils the list of abstract requirements enunciated in Sect. 2.2 and generalises other subclasses of the SnPR family while respecting the design philosophy on these. Hence, some previous results are still valid in the new framework. However, PC2Rnets can deal with more complex scenarios which were not yet addressed from the domain of SnPR nets. It should be remarked that no SnPR net class fulfils all requirements presented at the end of Sect. 2.2. Requirements 2–6 are satisfied by the S4PR class. Requirement 7 also is, but it is not fulfilled by Gadara nets. Requirement 1 is only verified by the Gadara and S*PR classes, and fulfilment of Requirement 8 has never been addressed before, justifying the next definition. Definition 2.2 presents a subclass of state machines used for modelling the control flow of the processes in isolation. Iterations are allowed, as well as decisions within internal cycles, in such a way that the control flow of structured programs can be fully supported, in fulfilment of Requirement 1. Definition 2.2. An iterative state machine N=hP, T, Ciis a strongly connected state machine such that: 1. Pcan be partitioned into three subsets: {pk},P1and P2. 2.3. The PC2R class 41 p0pk P1 P2                   Figure 2.3: Schematic diagram of an iterative state machine 2. P16=∅, 3. The subnet generated by {pk}∪P1,•P1∪P1•is a strongly connected state machine in which every cycle contains pk, 4. If P26=∅, the subnet generated by {pk} ∪ P2,•P2∪P2•is an iterative state machine. As Fig. 2.3 shows, P1contains the set of places of an outermost1iteration block, while P2is the set of places of the rest of the state machine (the inner structure, which may contain multiple loops within). Consequently, the subnet generated by {pk}∪P1,•P1∪P1•is a strongly connected state machine in which every cycle contains pk. Meanwhile, inner iteration blocks can be identified in the iterative state machine generated by {pk} ∪ P2,•P2∪P2•. Finally, the place p0represents the place “pk” that we choose after removing every iteration block. In the following, such possible last pkplaces will be generically called idle places. Note that by the definition of iterative state machine, at least one idle place must exist. Such term will serve as a bridge prior to the introduction of the concept of idle place of a process subnet in the context of the class of PC2Rnets. At this point, it must be remarked that the definition of iterative state machines is instrumental for introducing the class of PC2Rnets. In the net of Fig. 2.1, if we remove the resource places FORK1, FORK2 and BOWL, we obtain an iterative state machine, with P1={A2,A3,A4},P2= {A0,A5,A6}and pk= A1. Note that, according to the previous description, A0 can be considered the idle place. In the following, we assume that every state machine has one fixed idle place. Obviously, this idle place can be any place of the iterative state machine, but it is 1In the context of this thesis, we always use the adjectives outer /inner /etc. from the perspective of the structure of the iterative state machine: where the outermost iteration blocks are those farthest from the idle place. Please note that in the context of imperative programming languages is exactly the other way round: the innermost loops in the program structure are those which are modelled with the outermost iteration blocks in the iterative state machine. 42 2. The resource allocation problem in software applications assumed being identified from the beginning. Considering the application domain (multithreaded software engineering) this makes perfect sense, since an iterative state machine models the possible execution paths of a thread. In this sense, it must be remarked that the point of entry (thread startup) can be unequivocally identified by the begin statement. An elementary iteration block of an iterative state machine is a maximal strongly connected state machine embedded in the iterative state machine where all circuits contain a distinguished idle place named the idle place of the elementary iteration block. Algorithm 2.2 computes the set of these elementary iteration blocks and, in the answer, each elementary block is characterised by the idle place, pk, the set of places, PSM, and the set of transitions, TSM. Obviously, the flow relation between places and transitions of an elementary iteration block is the flow relation of the iterative state machine constrained to the objects of the elementary iteration block. Definition 2.3. Let N=hP, T, Cibe an iterative state machine, and p0∈Pbe its idle place. The set of elementary iteration blocks of N,SN, is the set generated by Algorithm 2.2. Note that the computation of a minimal circuit which covers a certain place p is a polynomial complexity problem that can be accomplished, for example, through the computation of a basic feasible solution via the SIMPLEX algorithm on the set of constraints C·x=0,x[p•]6=0,x≥0(basic feasible solutions are of minimal support and are therefore minimal t-semiflows of the net, i.e., elementary circuits). An analogous approach can be used to compute a minimal circuit containing a given transition. In the same vein, D. B. Johnson [Joh75] proposes an algorithm for the computation of minimal circuits of a digraph which starts by computing a first elementary circuit in polynomial time. Therefore Algorithm 2.2 exhibits a polynomial run-time growth rate on the size of the net in the worst-case scenario. Figure 2.4 depicts the elementary iteration blocks obtained for a sample iterative state machine using Algorithm 2.2, assuming that P0 is the idle place of the iterative state machine. In order to illustrate how it works, a trace of the first iterations of an execution of the algorithm using the net in Fig. 2.4 as input follows: idle pairs ={(P0,[P0 T1 P1 T3 P3 T6 P5 T8])}; Iteration 1 (idle place P0) pk= P0; π= [P0 T1 P1 T3 P3 T6 P5 T8]; ρ={P0,P1,P3,P5};PSM =∅;TSM ={T1,T3,T6,T8}; idle pairs =∅; Iteration 1.1 (place P0 ∈ρ) ρ={P1,P3,P5};p1= P0; τ= P0•\TSM ={T1,T2} \ TSM ={T2}; 2.3. The PC2R class 43 Algorithm 2.2 Splitting of an iterative state machine into its set of elementary iteration blocks Input: An iterative state machine N=hP, T, Ciand the idle place p0∈Pof N. Output: A set of strongly connected state machines of N,iteration blocks, each one with a distinguished idle place, and all circuits containing the detected idle place. Note 1: The function Min Circuit(N, x), x∈P∪T, returns a minimal circuit in N traversing x. Note 2: Given a circuit π, the functions fP(π) and fT(π) return the set of places and transitions, respectively, that occur at least once in π. begin 1: iteration blocks ← ∅;visited trans ← ∅;idle pairs ← {(p0,Min Circuit(N, p0))}; 2: while idle pairs 6=∅do 3: (pk, π)←Extract A Pair(idle pairs); 4: ρ←fP(π); PSM ← ∅;TSM ←fT(π); 5: while ρ6=∅do 6: p1←Extract An Element(ρ); 7: τ←p1•\(TSM ∪visited trans); PSM ←PSM ∪ {p1}; 8: while τ6=∅do 9: t←Extract An Element(τ); 10: π0←Min Circuit(N, t); 11: if pk/∈fP(π0)then 12: idle pairs ←idle pairs ∪ {(p1, π0)}; 13: else 14: ρ←(ρ∪fP(π0)) \PSM;TSM ←TSM ∪fT(π0); 15: end if 16: end while 17: end while 18: iteration blocks ←iteration blocks ∪ {(pk, PSM, TSM)}; 19: visited trans ←visited trans ∪TSM; 20: end while PSM =PSM ∪ {P0}={P0}; Iteration 1.1.1 (transition T2 ∈τ) t= T2; τ=∅;π0= [P0 T2 P2 T5 P4 T7 P5 T8]; pk∈fP(π0) =⇒ ρ={P1,P2,P3,P4,P5}; TSM ={T1,T2,T3,T5,T6,T7,T8}; Iteration 1.2 (place P1 ∈ρ) ρ={P2,P3,P4,P5};p1= P1; 44 2. The resource allocation problem in software applications T1 T7 T4 P1 P4 T2 T5 P2 T6 T3 P3 T8 P5 P0 T9 T10 P6 P7 T13 P8 T11 T12 T14 T15 P9 P10 T16 T17 P11 T19 T18 P12 T11 T12 Figure 2.4: Elementary iteration blocks of an iterative state machine τ= P1•\TSM ={T3,T4} \ TSM ={T4}; PSM ={P0,P1}; Iteration 1.2.1 (transition T4 ∈τ) t= T4; τ=∅;π0= [P0 T1 P1 T4 P4 T7 P5 T8]; pk∈fP(π0) =⇒ ρ={P2,P3,P4,P5}; TSM ={T1,T2,T3,T4,T5,T6,T7,T8}; Iteration 1.3 (place P2 ∈ρ) ρ={P3,P4,P5};p1= P2; τ= P2•\TSM ={T5,T9} \ TSM ={T9}; PSM ={P0,P1,P2}; Iteration 1.3.1 (transition T9 ∈τ) t= T9; τ=∅;π0= [P2 T9 P6 T10 P7 T13]; pk/∈fP(π0) =⇒ idle pairs =∅∪{(P2,[P2 T9 P6 T10 P7 T13])}; Iteration 1.4 (place P3 ∈ρ) ρ={P4,P5};p1= P3; τ= P3•\TSM ={T6} \ TSM =∅; PSM ={P0,P1,P2,P3}; Iteration 1.5 (place P4 ∈ρ) ρ={P5};p1= P4; 2.3. The PC2R class 51 As a consequence, there might exist additional minimal p-semiflows containing more than one resource place. This is also new and will be discussed in Subsection 2.3.3. In the following, BNdenotes the set of elementary iteration blocks of N, i.e., the set of elementary iteration blocks of each process subnet of N. Since all process subnets are disjoint, the shrinking graph associated to N,GN, is a forest of |IN| rooted trees holding the conditions of Lemma 2.10. The next definition is strongly related to the notion of acceptable initial marking introduced for the S4PR class. In software systems all processes/threads are initially inactive and start from the same point (the begin statement). Hence, all of the corresponding tokens are in the idle place at the initial marking (the process places being therefore empty). The definition takes this into account and establishes a lower bound for the marking of the resource places. Definition 2.13. Let N=hP0∪PS∪PR, T, Cibe a PC2Rnet. An initial marking m0 is acceptable at level 0 (0-acceptable) for Niff km0k\PR=P0, and ∀p∈PS, r ∈PR: yrT·m0=m0[r] + X p0∈P0∩kyrk yr[p0]·m0[p0]≥yr[p] . Note that Definition 2.13 traces a lower bound for the initial marking of each resource place r∈PR(namely, ∀p∈PS:m0[r]≥yr[p]−Pp0∈P0∩kyrkyr[p0]·m0[p0]). If the marking of some resource place is below that bound, then there exists at least one dead transition at the initial marking, as later proved in Subsection 2.4.1. But having a marking which is above that bound does not guarantee, in the general case, that there do not exist dead transitions. Again, all of this is more profoundly discussed in Subsection 2.4.1. Nevertheless, it is worth stressing at this point that an S4PR net system with an acceptable initial marking cannot have any dead transition at the initial marking (since every minimal t-semiflow is firable in isolation from it). Hence the use of the suffix at level 0 in Definition 2.13, in spite of introducing a concept which collapses with the definition of acceptable initial marking for the S4PR subclass, as proved a bit later in Subsection 2.3.3. By refining this definition, the fact that they may induce different behavioural patterns in the general case is stressed. Note that in earlier works [LGC12], this refining is not used. However, it is introduced here for the sake of clarity. Note that in the following, when the context does not allow any ambiguity, the term acceptable initial marking may be used to refer to 0-acceptable initial markings in a more concise way. Finally, note that resource places whose support includes some idle place may be empty for a 0-acceptable initial marking. Figure 2.2 shows a PC2Rnet with a 0-acceptable initial marking. This net does not belong to the S4PR subclass. 52 2. The resource allocation problem in software applications 2.3.3 Hierarchy of classes and p-semiflows In the following definition we stress the main differences between the well-known classes of the SnPR family. Observe that these differences are essentially associated to the places belonging to the support of the p-semiflows of the resources. Definition 2.14. Previous classes of the Sn PR family are defined as follows: •An S5PR net [LGC06] is a PC2Rnet where ∀r∈PR:kyrk ∩ P0=∅. •An S4PR net [Tri03,TGVCE05] is an S5PR net where ∀i∈INthe subnet generated by {p0i} ∪ Pi, Tiis a strongly connected state machine in which every cycle contains p0i(i.e., a iterative state machine with no internal cycles). •An S3PR net [ECM95] is an S4PR net where ∀p∈PS:|••p∩PR|= 1 and ••p∩PR=p•• ∩PR. •An L-S3PR net [EGVC98] is an S3PR net where ∀p∈PS:|•p|=|p•|= 1. Remark 2.15. L-S3PR ⊆S3PR ⊆S4PR ⊆S5PR ⊆PC2R. The preceding remark is straightforward from Definition 2.14. It is worth noting that Definition 2.13 collapses with the definition of acceptable initial markings respectively provided for those subclasses [ECM95,EGVC98,TGVCE05]. That for the S4PR subclass is provided in Definition 1.2. In a similar vein, we can define the concept of acceptable initial marking for the S5PR subclass: Definition 2.16. Let N=hP0∪PS∪PR, T, Cibe an S5PR net. An initial marking m0is acceptable for Niff km0k \ PR=P0, and ∀p∈PS, r ∈PR:m0[r]≥yr[p]. The latter also collapses with Definition 2.13, since yrT·m0=yr[r]·m0[r] + Pr0∈PR\{r}(yr[r0]·m0[r0]) + Pp∈PS(yr[p]·m0[p]) + Pp0∈P0(yr[p0]·m0[p0]) = m0[r] (mind that, by Definition 2.12,yr[r] = 1,kyrk ∩ PR={r}and m0[PS] = 0and, by Definition 2.14,kyrk ∩ P0=∅). Besides, there exists another class for Sequential RASs, called SPQR [LGC06], which is dealt with in Sect. 2.5. This class does not strictly contain or is contained by the PC2Rclass. Yet, there exist transformation rules to travel between PC2Rand Structurally Bounded (SB) SPQR nets. Note that, by construction, PC2Rnets are conservative, and hence SB, but this is not true for SPQR nets. The SPQR class seems interesting from an analytical point of view thanks to its syntactic simplicity, as discussed in Subsection 2.5. One perspective for inspecting the differences between the subclasses of PC2Ris that of the form and number of minimal p-semiflows. All subclasses are conservative by definition. Let ySidenote the unique minimal p-semiflow induced by the iterative state machine generated by restricting Nto h{p0i} ∪ Pi, Tii. 2.3. The PC2R class 53 Lemma 2.17. Let N=hP, T, Cibe a PC2Rnet. A basis of the left null space of the incidence matrix Ccontains |PR|+|IN|vectors. Proof. For every r∈PR, let y− r=yr−Pi∈INyr[p0i]·ySi. The set of vectors A={ySi|i∈IN}∪{y− r|r∈PR}contains |PR|+|IN|vectors and they are linearly independent, because for each p∈PR∪P0there exists one and only one distinct vector y∈Asuch that y[p] = 1 and ∀y0∈A,y06=y,y0[p] = 0. Moreover, Ais a basis because there is no other vector linearly independent with the vectors of A. This last statement is proved by contradiction. Let us suppose that there exists ybeing a left annuller of Cand ycannot be generated from vectors of A. Construct the vector y0=y−Pi∈INy[p0i]·ySi−Pr∈PRy[r]·y− r. Obviously, y0is a left annuller of N because so are the vectors of Aand y, but ky0k ⊆ PS, and this is not possible because there are no annullers of the iterative state machines without their idle places. Now let Bbe a matrix of dimensions (|PR|+|IN|)× |P|of integers such that the rows of Bare the set of vectors Adefined in the previous proof. Lemma 2.18. If Nis an S5PR net, Bis a non-negative canonical basis of psemiflows. Proof. By reordering columns in Bso that the first ones correspond to PR∪P0, and subsequently reordering the rows of B, a matrix of the form [I|B0] is obtained, where Iis the identity matrix of dimension |PR|+|IN|, and B0is a matrix of dimensions (|PR|+|IN|)× |PS|of non-negative integers, since in S5PR nets, ∀r∈PR,yr[P0]=0 and y− r=yr. Corollary 2.19. If Nis an S3PR net, then every row in Bbelongs to {0,1}|P|. However, nets belonging to the S4PR class may have non-binary minimal psemiflows. Furthermore, PC2Rnets feature a new kind of minimal p-semiflows: Lemma 2.20. If Nis a PC2Rnet but not an S5PR net, there exists at least one minimal p-semiflow whose support contains more than one resource place. Proof. Since Nis not an S5PR net, there exists r∈PR,i∈INsuch that p0i∈ kyrk. In that case, there exists at least one p∈Pisuch that p /∈ kyrk(otherwise, yr−ySi≥0and yris not minimal). Let Abe the minimal set of minimal p-semiflows, {yu|u∈PR}, that are essential to cover every p∈Pisuch that yr[p] = 0. This means that yu∈Aiff ∃p∈Pi,yr[p] = 0, yu[p]6= 0 and ∀yv∈A,yv6=yu:yv[p] = 0. By Definition 2.12.5, this set Aexists. We construct y0 r=yr+Pyu∈Ayu, that obviously contains, at least, the p-semiflow ySi. Therefore, y− r=y0 r−k·ySi, k = minp∈kySik{y0 r[p]}, is a p-semiflow by construction, and y− r[PR] = y0 r[PR]. In the same way, we detract other ySjthat can be contained in y− r. If y− ris a minimal p-semiflow then the lemma is true, since the support of y− r contains more than one resource place. Otherwise, three facts must be considered: 54 2. The resource allocation problem in software applications 1. By construction, y− rcannot contain any ySj,∀j∈IN, since all those have been maximally detracted. 2. The p-semiflow y− rdoes not contain any minimal p-semiflow yvcovering one single resource place. By contradiction. Let us suppose that y− rcontains yv. The resource vmust be either ror a resource for which its minimal p-semiflow yvis in A. If vis rthen yv[r] = y− r[r], and (y− r−yv)[p0i]<0. Therefore, a contradiction is reached. If vholds yv∈Athen yv[v] = y− r[v] because the weight y− r[u] is not modified by the previous operations. And (y− r−yv)[p]<0 for some p∈Pifor which yvbecomes essential in the set A, since y− r[p]≤ yv[p]−k. 3. Last, there must exist one minimal p-semiflow y−− rsuch that ky−− rk⊂ky− rk (otherwise, y− ris minimal). Considering the two previous facts, the support of y−− rcontains more than one resource place. In other words, the above result reveals that the set of minimal p-semiflows contains strictly a basis of the left null space of the incidence matrix C. 2.3.4 Basic structural properties Trivially, the next lemma follows: Lemma 2.21. Every PC2Rnet is conservative. On the other hand, each PC2Rnet is consistent, and so is every net belonging to the rest of subclasses. Lemma 2.22. Every PC2Rnet is consistent. Proof. Let Nbe a PC2Rnet. The process subnets of Nare strongly connected state machines (indeed, they are iterative state machines) and therefore each one is consistent, i.e., every transition tof Nis covered by at least a t-semiflow of the iterative state machine containing t. It will be proved that these t-semiflows are also t-semiflows of the net N. Indeed, if xis a t-semiflow of Nwithout resources it is enough to prove that ∀r∈PR:C[r, T]·x= 0. Taking into account Definition 2.12, point 4, C[r, T ] = −Pp∈kyrk\{r}yr[p]·C[p, T], and therefore: C[r, T ]·x=− X p∈kyrk\{r} yr[p]·C[p, T] ·x=−X p∈kyrk\{r} yr[p]·C[p, T]·x= 0. Hence, Nis consistent. 2.3. The PC2R class 55 Observe that conservative and consistent nets are called well-formed nets [Ter04] because this is a necessary condition for structural liveness and structural boundedness. The next lemma is rather obvious and a well-known result in the Petri net literature but, for practical reasons, it is nonetheless stated for our restricted class of nets since it will often be used in proofs of this and some other forthcoming chapters. Lemma 2.23. Let Nbe a conservative P/T net, and y∈IN|P|be a p-semiflow of N. The support of y,kyk, is both a siphon and a trap of the net. Proof. Since yis a p-semiflow, each column of the incidence matrix must be annulled by y, i.e., y·C[P, t] = 0, for every t∈T. In order to annul each column for its corresponding transition tin the set •(kyk)∪(kyk)•at least one input and one output place of tis needed. Therefore •(kyk) = (kyk)•, i.e., kykis both a siphon and a trap. Now an analogous lemma can be stated for the dual case of t-semiflows. This lemma plays an instrumental role in subsequent proofs. Lemma 2.24. Let Nbe a consistent P/T net. Every t-semiflow xof Nholds •kxk= kxk•. Proof. The dual net of a consistent net is a conservative net. By Lemma 2.23, the dual p-semiflow of xis the support of both a siphon and a trap. Then •kxk=kxk•. The proof of Lemma 2.22 shows that a minimal circuit is always the support of a t-semiflow (and vice versa). On the other hand, Lemma 2.6 proves that each minimal circuit is local to a unique iteration block. Therefore, the next lemma is closely related to the conservativeness in the use of resources within the circuits of an elementary iteration block. The conservativeness for the whole elementary iteration block is finally proved by Lemma 2.26. Lemma 2.25. Let Nbe a well-formed P/T net, and xbe a t-semiflow of N. The subnet induced by x, i.e., the subnet generated by •kxk,kxk, is conservative. Proof. Nis conservative, i.e., ∃y∈IN|P|,y>0:yT·C=0. Therefore, ∀t∈ kxk: yT·C[t] = 0. Since, by Lemma 2.24,•kxk=kxk•, then C[P\•kxk,kxk] = 0. Therefore, yT[•kxk]·C[•kxk,kxk] = 0and the lemma holds. Lemma 2.26. Let Nbe a PC2Rnet, and B= (p, PSM, TSM)be an elementary iteration block of a process subnet of N,B∈BN. The use of resources in Bis consistent and conservative (i.e., the subnet generated by •TSM,TSM is consistent and conservative). 56 2. The resource allocation problem in software applications Proof. Lemma 2.11 proves that every elementary iteration block is consistent in isolation. Since Nis a state machine, the t-semiflow that covers all the transitions in the block is also a t-semiflow of N. On the other hand, Lemma 2.25 proves that the subnet induced by a t-semiflow in Nis conservative. Therefore, the use of resources in Bis conservative. The above result states that not only a PC2Rnet is globally well-formed, but also that so is every elementary iteration block augmented with the resource places it interacts with, considered from a local perspective. Finally, we want to formalise that PC2Rnets correspond to an RAS view of systems since the so-named resource places have a behaviour according to the actual experience or intuition that software engineers have about conservative resources. This means that if we have enough copies of a type of resource then it is not a constraint to the system of processes and can be removed from the analysis of the RAP. This intuitive idea is captured in Petri nets by means of the concept of Structurally Implicit Place (SIP). An SIP is a place whose row in the incidence matrix can be obtained as a non-negative linear combination of other rows of the incidence matrix. This property, essentially a structural property, leads to that if we have the freedom to select the initial marking for these places, we can make them implicit places and then they can be removed from the net maintaining the same set of occurrence sequences of transitions. The next result points out this structural property. Lemma 2.27. Let Nbe a PC2Rnet and ra resource place of N. The place ris structurally implicit and C[r, T] = −X p∈kyrk\{r} yr[p]·C[p, T] + X ∀i:kySik∩kyrk6=∅ Ki·ySi, where Ki= max{yr[p]|p∈ kySik}. Proof. The result is trivially true because from the definition of PC2Rnet, there exists a unique p-semiflow such that {r}=kyrk ∩ PR, (P0∪PS)∩ kyrk 6=∅and yr[r] = 1. Therefore, pre-multiplying the incidence matrix by the vector yr, we can construct the following equation: C[r, T] = −X p∈kyrk\{r} yr[p]·C[p, T] Obviously, this is a non-negative linear combination of rows of the incidence matrix. But we know that, for each iterative state machine i, there exists a minimal psemiflow ySi∈ {0,1}|P|that we can add to the previous equation because ySi T·C= 0, but weighted by the greatest coefficient yr[p] of those places pbelonging to the i-th 2.3. The PC2R class 57 R1 R2 R3 T1 T3 T2 A1 A2 T4 T5 T6 B1 B2 B0 A0 Figure 2.6: A rather simple PC2R net iterative state machine. Applying this procedure to all iterative state machines visited by the p-semiflow of rwe obtain a non-negative linear combination of rows of the incidence matrix as follows: C[r, T] = −X p∈kyrk\{r} yr[p]·C[p, T] + X ∀i:kySik∩kyrk6=∅ Ki·ySi where Ki= max{yr[p]|p∈ kySik}. That is, ris a structurally implicit place. Observe that this linear combination of process places and possibly some idle places is unique. Nevertheless, we can have other linear combinations including not only process places or idle places, but also other resource places present in the net. For example, in the net depicted in Fig. 2.6, if we consider the resource place R2, we have two different equations to obtain the row of R2 in the incidence matrix: C[R2,·] = C[A0,·] + C[A2,·] + C[B1,·] C[R2,·] = C[R1,·] + C[R3,·] + C[A2,·] Observe that, in the first equation, the implying places are only process places, A2 and B1, as well as the idle place A0. Nevertheless, the second equation contains as implying places the resources R1 and R3. According to the theory of structurally implicit places [GVC99], if we are considering SIPs in structurally bounded nets then we can compute a finite initial marking for a SIP making it an implicit place. For example, we can compute a bound of the minimal initial marking for the place R2 in the net of Fig. 2.6 to make it implicit. This is accomplished by resolving a linear programming problem [GVC99]. The obtained result is 2, that is, the minimum initial marking for the place R2 to be implicit is equal to 2. Therefore, R2 in the figure is implicit. 58 2. The resource allocation problem in software applications This small value for this initial marking of the place R2 is due to the second previous equation because the more restrictive places to the firing of the output transitions of place R2 are the resource places and not the process and idle places of the first equation. This apparently instrumental result allows us to obtain interesting conclusions. The first one says that we must analyse if the resources of a PC2Rnet system are implicit or not, because if some of them are implicit, we can remove them and then we can simplify further analysis (less siphons, for example) or even we can fall in a subclass where we can find stronger results that can be applied. The second conclusion says that we can conclude that these nets are structurally live and structurally bounded. Lemma 2.28. Every PC2Rnet is structurally live and structurally bounded Proof. The net is conservative, therefore it is structurally bounded. All resource places are structurally implicit places, therefore if we consider an initial marking where: (i) All resource places have an initial marking making each one implicit; and (ii) All idle places contain at least one token; then the net is live. In effect, if the resource places are implicit then we can remove them and the language of occurrence sequences remains unchanged. Therefore, the resulting net is composed by a set of strongly connected state machines, each one containing at least one token, and therefore, each one is live. If our net is live, is structurally live. That is, structural implicitness of resources, and the acceptable initial markings guarantees structural liveness and structural boundedness in PC2R. 2.4 A cross-sectional view on the liveness analysis problem So far, it has been introduced a Petri net class (the PC2Rclass) which fulfils the list of basic model requirements introduced in Sect. 2.2. In this section, it is proved that finding a structural characterisation of the liveness problem reveals itself much harder than was for previous (sub-)classes used in the FMS context. The discussion is divided into three parts. In Subsection 2.4.1, the hard problem of establishing an acceptable initial marking in general PC2Rnets is investigated. This problem was trivial for earlier net subclasses in the SnPR family. In Subsection 2.4.2, it is reminded how siphons structurally capture the problem of liveness in those subclasses, and evidenced that this kind of siphons is no longer sufficient to characterise non-liveness in the multithreaded software domain. Finally, in Subsection 2.4.3, some other properties strongly related to liveness analysis are inspected. 2.4. A cross-sectional view on the liveness analysis problem 59 2.4.1 Acceptability of the initial marking: The 0-1 zone In Subsection 2.3.2 it was introduced the notion of 0-acceptable initial marking. As explained there, it is a generalisation of the notion of acceptable initial marking which was introduced for the SnPR subclasses (see, e.g., Definition 1.2 for S4PR, and Definition 2.16 for S5PR). One common factor in those subclasses is that any initial marking which is not acceptable just because of a lack of tokens in the resource places (i.e., it is not acceptable in spite of having km0k \ PR=P0) guarantees that there is a dead transition at the initial marking (and therefore the net system is non-live). Thus, this kind of markings can be discarded from the very beginning. This is a property which can be extended to PC2Rnets and 0-acceptable initial markings. The next theorem proves that. Although it can be trivially extended for a more general class of conservative Petri nets, it is specialised here for PC2Rnets for the sake of clarity: Theorem 2.29. Let hN ,m0ibe a PC2Rnet system with an initial marking such that km0k \ PR=P0but ∃p∈PS,y∈IN|P|such that yT·C=0and yT·m0<y[p]. Then at least one transition is dead at m0. Proof. By multiplying both sides of the net state equation by yTwe get: yT·m= yT·m0+yT·C·σ=yT·m0. Thus, for every m∈RS(N,m0) : 0 ≤yT·m= yT·m0<y[p]. Since m,y≥0then y[p]·m[p]≤yT·m<y[p], and therefore m[p] = 0. Thus pis empty for every reachable marking, so all its input and output transitions must be dead. Nevertheless, another common factor for the S5PR and simpler subclasses is that having an acceptable initial marking guarantees that every minimal t-semiflow is eventually realisable from the initial marking. This ultimately implies that every transition is firable an arbitrary number of times since these nets are consistent by Lemma 2.22. This is later discussed in Subsection 2.4.3 and proved in Theorem 2.40. On the contrary, there exist PC2Rnet systems with 0-acceptable initial markings such that there exist dead transitions at those initial markings. In some cases, the observation of a set of minimal p-semiflows provides enough information to infer the deadlock. In those cases, at least one of the minimal p-semiflows must have two or more resource places in its support (i.e., the set cannot be a subset of A, as defined in Subsection 2.3.3). As a result, such nets cannot belong to the S5PR subclass, since in that case every p-semiflow belongs to the set Aby Lemma 2.18. One of such nets is depicted in Fig. 2.7. The net also proves that the reverse of Theorem 2.29 is false in general for the PC2Rclass: in this case, no (minimal) psemiflow provides enough information when observed isolately. This is straightforward 60 2. The resource allocation problem in software applications 2 T2 T3 A1 A2 A0 R2 R1 C1 R4R3 T7 T8 C0 T4 T5 T6 B2 B1 B0 22 24 3 2 T1 A02, B02, C0, R1, R2 T1 A0, A1, B02, C0, R2, R3 A0, A2, B02, C0, R1, R32 T2 T3 A0, A2, B0, B1, C0, R32, R4 A02, B0, B1, C0, R2, R4 A02, B0, B2, C0, R1, R44 A0, A1, B0, B2, C0, R3, R44 T4 T3 T4 T5 T6 T1 T6 A1, A2, B02, C0, R33A02, B1, B2, C0, R45 T1 T4 T3 T6 Figure 2.7: Non-live PC2R net system with a 0-acceptable initial marking. No (minimal) p-semiflow reveals, when considered in isolation, that T7 and T8 are dead at m0 from the complete set of minimal p-semiflows, represented by the following place invariants: m[A0] + m[A1] + m[A2] = 2 m[B0] + m[B1] + m[B2] = 2 m[C0] + m[C1] = 1 m[R1] + m[A1] + m[B1] = 1 m[R2] + m[A2] + m[B2] = 1 m[R3] + 2 ·m[A0] + m[A1] + 2 ·m[C1] = 4 m[R4] + 4 ·m[B0] + 3 ·m[B1] + 2 ·m[C1] = 8 2·m[R1] + 4 ·m[R2] + 2 ·m[R3] + m[R4] + m[B1] + 6 ·m[C1] = 6 m[R1] + 4 ·m[R2] + 3 ·m[R3] + m[R4] + 2 ·m[A0] + 8 ·m[C1] = 9 m[R1] + 4 ·m[R2] + m[R3] + m[R4] + 2 ·m[A2] + 4 ·m[C1] = 5 m[R1] + 4 ·m[R2] + m[R4] + m[A1] + 4 ·m[A2] + 2 ·m[C1] = 5 3·m[R2] + 3 ·m[R3] + m[R4] + 3 ·m[A0] + m[B0] + 8 ·m[C1] = 11 3·m[R2] + m[R4] + 3 ·m[A2] + m[B0] + 2 ·m[C1] = 5 m[R1] + 2 ·m[R2] + m[R3] + m[B1] + 2 ·m[B2] + 2 ·m[C1] = 3 m[R2] + m[R3] + m[A0] + m[B2] + 2 ·m[C1] = 3 Nevertheless, the fact that there exist dead transitions can be determined from the 2.4. A cross-sectional view on the liveness analysis problem 67 K R2 R3 R4 R1 TB2 1 3 TA1 TA5 TA4 TA3 TA6 A5 A4 A3 A1 TA2 A2 A0 TB7 TB3 TB8 TB4 TB5 TB1 B0 B1 B3 B4 B5 TB6 B2 K 0 KTA7 Figure 2.12: S3PR net which is non-live iff (K0≥K1, K3≥2) ∨(K0·K1·K3= 0). Note that m0is an acceptable initial marking iff (K0·K1·K36= 0) transition is m-resource-disabled by resource places in D;iii) Process places in Dare empty at m. Such a siphon Dis said to be insufficiently marked at m. In Theorems 2.32 and 2.33, the siphon captures the concept of circular wait, revealing it from the underlying net structure. In contrast to the S3PR class, it is worth noting the following fact about minimal siphons in S4PR net systems, which emerges because of their minimal p-semiflows not being strictly binary. Property 2.34. There exists an S4PR net system with an acceptable initial marking which is non-live but every siphon pointing out the non-liveness is non-minimal, i.e., minimal siphons are non-sufficient to characterise non-liveness. For instance, the S4PR net system in Fig. 1.4 is non-live, but there is no minimal siphon containing both resource places R1 and R2. Note that the siphon D= {R1,R2,A3,B2}becomes insufficiently marked at m, where m≡[A1,B1,R1,R2], but it contains the minimal siphon D0={R2,A3,B2}.D0is not insufficiently marked for any reachable marking. The problem is that the unique resource place of D0(i.e., R2) is not disabling every m-process-enabled transition. Thus the resource place R1 is needed to decide that all m-process-enabled transitions are m-resource-disabled. Another interesting peculiarity of this net system is that no siphon is ever emptied. Thus non-minimal siphons must be considered in order to deal with deadlocks in systems more complex than S3PR. On the other hand, insufficiently marked siphons (even considering those nonminimal) are not enough for characterising liveness for more complex systems such as 68 2. The resource allocation problem in software applications S5PR models. This means that siphon-based control techniques for RASs do not work in general for concurrent software, even in the ‘good’ case in which every wait-like operation precedes its complementary signal-like operation. Property 2.35. There exists an S5PR net system with an acceptable initial marking hN,m0iwhich is non-live but insufficiently marked siphons do not point out nonliveness (dead markings). The S5PR net system in Fig. 2.13 evidences the claim stated above. The figure depicts a non-live system with three possibly bad minimal siphons. These siphons are D1={A2,A3,A4,A5,A6,B2,B4,B5,B6,FORK2,BOWL},D2= {A2,A4,A5,A6,B2,B3,B4,B5,B6,FORK1,BOWL}and D3={A2,A4,A5,A6, B2,B4,B5,B6,FORK1,FORK2,BOWL}. Besides, every transition in the set Ω = {TA2,TA3,TA4,TA5,TB2,TB3,TB4,TB5}is an output transition of D1,D2and D3. After firing transitions TA1 and TB1 starting from m0, the state [A1,B1,BOWL] is reached. This marking belongs to a livelock with other six markings. The reader can check that (i) there exists a firable transition in Ω for every marking in the livelock, (ii) the rest of transitions cannot be fired anymore (the net is non-live), and (iii) in any case there is no insufficiently marked siphon. Revisiting Example 2.1 and its associated Algorithm 2.1, it is not difficult to see that, if every philosopher enters the room, sits down and picks up the fork on the left of himself, the philosophers will be trapped in a livelock. Any philosopher can eventually take the bowl of spaghetti and heat it up in the microwave. This pattern can be repeated infinitely often, but it is completely useless, since no philosopher will ever be able to have dinner. This behaviour is obviously reflected in the corresponding net representation at Fig. 2.2. Let us construct a firing sequence σcontaining only the first transition of each state machine (i.e., the output transition of its idle place). The firing order of these transitions is irrelevant. Now let us fire such a sequence, and the net falls in a livelock. The internal cycles are still firable in isolation, but no idle place can ever be marked again. Unfortunately, the net has several bad siphons, but none of them is empty or insufficiently marked in the livelock. In other words, for every reachable marking in the livelock, there exist output transitions of the siphons which are firable. As a result, the siphon-based non-liveness characterisation for earlier net classes (such as S4PR [TGVCE05]) is not sufficient in the new framework. 2.4.3 Deadlock-freeness, liveness, reversibility and livelocks By carefully observing the net in Fig. 2.13, it might seem that the difficulty in finding a liveness characterisation for PC2Rnet systems lies in the appearance of certain types of livelocks. In general, livelocks with dead transitions are not a new phenomenon in 2.4. A cross-sectional view on the liveness analysis problem 69 A3 TB6 TB7 TA1 TA8 TA7 TA6 FORK1 FORK2 BOWL TA5 TA2 A4 A6 A5 A1 A0 B0 B5 B6 B1 TB8 TB1 B2 TB2 TB5 A2 B4 TB3 B3 TA3 TA4 TB4 A0, B0, FORK1, FORK2, BOWL A1, B0, FORK2, BOWL TA1 A0, B1, FORK1, BOWL TB1 A5, B0 TA8 TA7 TA6 A0, B5 TB8 TB7 TB6 A1, B1, BOWL TB1 TA1 A2, B0, FORK2 A0, B2, FORK1 TB2 A2, B1 TA2 A1, B2 TB2 A4, B1 A1, B4 TA4 TB4 TA5TB5 A3, B1, FORK1 A1, B3, FORK2 TA3 TB3 TA2 TA5 A3, B0, FORK1, FORK2 TA3 TA4 TB1 TB1 TB1 TB5 A0, B3, FORK1, FORK2 TB3 TA1 TA1 TA1 TB4 A4, B0, FORK2 A0, B4, FORK1 A6, B0, BOWL A0, B6, BOWL Figure 2.13: Non-live S5PR net system modelling two postmodern dining philosophers the context of Petri net models for RASs. Figure 2.14 shows that, even for L-S3PR nets, deadlock-freeness does not imply liveness. Property 2.36. There exists a L-S3PR net system with an acceptable initial marking such that it is deadlock-free but not live. This L-S3PR net system has no deadlock but two reachable livelocks: Livelock1 ≡ {[A0,B2,C0,D1,R1],[A1,B2,C0,D1]} Livelock2 ≡ {[A0,B1,C0,D2,R3],[A0,B1,C1,D2]} 70 2. The resource allocation problem in software applications D3 A0 C1 A1 C0 TC2 TC1 TA2 TA1 R2 R1 R3 TD4 TD1 TB1 TB4 TB2 TB3 TD3 TD2 B0 D0 B1 B2 B3 D1 D2 Figure 2.14: Non-live but deadlock-free L-S3PR net system Nevertheless, these livelocks are captured by insufficiently marked siphons. Unfortunately, this no longer holds for some kind of livelocks in S5PR or more complex systems. Indeed, PC2Rnets feature some complex properties which complicate the finding of a liveness characterisation. Another relevant property for studying liveness is its monotonicity. In spite of the seeming simplicity of S3PR nets, the following negative result regarding liveness monotonicity applies: Property 2.37. There exists an S3PR net such that liveness is not monotonic, either with respect to the marking of the idle/process places, or that of the resource places, i.e., liveness is not always preserved when those are increased. The net depicted in Fig. 2.12 illustrates this fact: •With respect to PR: The system in Fig. 2.12 is live with K0= K1= K3= 1 and non-live with K0= K1= 1, K3= 2 (however, it becomes live again if the marking of R1, R2 and R4 is increased enough so as to make every resource place an implicit place). •With respect to P0: The system in Fig. 2.12 is live with K0= 1, K1= K3= 2 and non-live with K0= K1= K3= 2. Note that liveness is monotonic with respect to the marking of the resource places for every net belonging to the L-S3PR class [GV99]. But, from S3PR nets upwards, there is a discontinuity zone (i.e., a range of initial markings where the property is fluctuating) between the point where the resource places are empty enough so that every transition is dead (also held for lower markings), and the point where every resource place is implicit (liveness is preserved if their marking is increased). Markings within these bounds fluctuate between liveness and non-liveness. The location of those points also depends on the marking of the idle/process places: the more tokens in them, the farther the saturation point (i.e., the upper bound). 2.4. A cross-sectional view on the liveness analysis problem 71 m0(Ri) m0(Rj) The net is non-live Frontier: Every resource place is implicit 0 0 8 + 8 + Some transition is already dead at m 0 Level 1 of acceptability of initial markings (1-acceptable) The net is live (but no transition is dead yet at m 0 ) Figure 2.15: Schematic of the liveness discontinuity zone for marked PC2R nets. It is assumed that km0k \ PR=P0and that m0[P0∪PS] remains fixed. Note that there may exist m0making the system non-live at the 0-1 zone (i.e., below the ‘1-acceptable’ frontier) Note that, as discussed in Subsection 2.4.1, for PC2Rnets liveness is also neither monotonic for those markings in the 0-1 zone (more exactly, above the frontier of markings which separates those systems with dead transitions and those without). Figure 2.15 depicts this. Nevertheless, an interesting property of S4PR net systems is that liveness is a necessary and sufficient condition for reversibility. This, along with the fact that the idle place does not belong to any p-semiflow yr, is a powerful feature. If every token in a process net can be moved to the idle place, then the net is not dead (yet). Theorem 2.38. Let hN,m0ibe an S4PR net system with an acceptable initial marking. hN,m0iis live iff m0is a home state (i.e., the system is reversible). Proof. =⇒)Let us suppose that m0is not a home state, i.e. ∃m0∈RS(N,m0) such that m0/∈RS(N,m0). Let m∈RS(N,m0) obtained by moving forward all the active processes (firing transitions T\P0•) until no process enabled transition can be fired. Since m0/∈RS(N,m0), m6=m0, and the set of mprocess-enabled transitions is non-empty, and each one of these transitions is m-resource-disabled. Hence, by Theorem 2.33,hN,m0iis non-live. 72 2. The resource allocation problem in software applications ⇐=)Let mbe a reachable marking from m0,m∈RS(N,m0), and ta transition of the net. It will be proved that there exists a successor marking of m,m0, from which tis firable. Since m0is a home state, there exists a firable sequence from msuch that mσ −→m0. Taking into account that every t-semiflow can be fired in isolation from an acceptable initial marking of an S4PR net [Tri03], then there exists a sequence σ0whose characteristic vector σ0is equal to the t-semiflow containing t(this t-semiflow exists because the net is consistent by Lemma 2.22). Let σ0=σ0 1t σ0 2be a decomposition of the firing sequence σ0to point out the first firing of t. Therefore σ σ0 1is firable leading to a marking m0 from which tis firable. Because mand thave been selected without constraints, the net is live. However, Theorem 2.38 is false in general for S5PR nets. In fact, the directedness property [BV84] does not even hold. This implies that an S5PR net system may not have a home state, even being live. Property 2.39. There exists an S5PR net system with an acceptable initial marking hN,m0isuch that the system is live but there is no home state. The net system in Fig. 2.16 is a S5PR which has no home state in spite of being live. It is worth noting that this net is ordinary. The reachability graph is illustrated in Fig. 2.17. Having said that, S5PR nets still retain an interesting property: its minimal tsemiflows are eventually realisable from an acceptable initial marking. Theorem 2.40. Let hN,m0ibe an S5PR net system with an acceptable initial marking. For every (minimal) t-semiflow x, there exists a reachable marking m∈ RS(N,m0)such that xis realisable from m, i.e. ∃σsuch that mσ −→,σ=x. Proof. This is straightforward from Theorem 2.31, since an acceptable initial marking for an S5PR net is also a 1-acceptable initial marking (both definitions collapse for this subclass). However, for PC2Rnet systems there may not exist minimal t-semiflows being eventually realisable; even for live systems. Property 2.41. There exists a PC2Rnet system with a 0-acceptable initial marking hN,m0isuch that the system is live and there exists a minimal t-semiflow xsuch that ∀m∈RS(N,m0),@σsuch that mσ −→ and σ=x, i.e. xis not realisable from any m∈RS(N,m0). 2.4. A cross-sectional view on the liveness analysis problem 73 R1 R2 R3 R4 R6R5 B2 T15 B3 T16 T13 T14 B4 B5 T19 B7 B8 T23 T17 T18 T21 T22 B10B9 T24 T25 T26 B11 T27 B6 T20 B0 R6 R5 R7 R6 R14 B1 R4 R10 R11R12 R14 R10 R4 R12R11 R14 R4 R9 R11R10 R12 R9 R4 R10R11 R12 R7 R3 R9 R6 R8 R7 R9 R13 R4 R10 R2R4 R8 R10 R12 R5 R8 R13 R7 R14 R3 R5 R9 R3 R5 R6 R3 R9 R2 R8 R12 R2 R4 R9 R10 R14 R1 R9 R5 R14 R6 R5 R7 R6 R5 R7 R8 R6 R11R5 R8 R7 R6 R8 R11 R3 R2 R10 R4 R8 R2 R3 R4 R10 R8 R12 R4 R10 R14 R9 R1 R14 R7 R8 R2 R9 R12 A1 T11 A9 T1 A8A2 T3 A3 T4 A4 T5 A5 T8 A7 T9 T12 A6 T10 T2 T6 T7 A0 R7 R8 R14R13R12R11R10R9 Figure 2.16: Live S5PR net system which has no home state. The arcs from/to PRare omitted for clarity. Instead, the set of input and output resource places are listed next to each transition The reader can check that the PC2Rnet system in Fig. 2.9 has no home state in spite of being live. Depending on which transition is fired first (either T1 or T8) a different livelock is reached. Besides, for every reachable marking, there is no minimal t-semiflow such that it is realisable, i.e. firable in isolation. Instead, both state machines need each other to progress in an interleaved way from the very beginning. T-semiflow realisability is, however, guaranteed when the initial marking is a 1acceptable initial marking, by Theorem 2.31. Obviously, the initial marking in the net of Fig. 2.9 does not hold this, in spite of being a 0-acceptable initial marking. Counterintuitively, the impossibility of realising every t-semiflow in a live PC2R net system cannot be directly linked to non-reversibility. The net system in Fig. 2.9 has no home state. However, the net system in Fig. 2.18 is reversible, live, but no minimal t-semiflow is realisable. In fact, these two properties (reversibility and t-semiflow realisability) are usually strongly linked to the property of liveness for many Petri net classes. Particularly, reversibility is powerful since its fulfilment implies that the net is live iff there are no dead transitions at the initial marking. This last property is often easy to check (although that statement is not true in general for PC2Rnet systems, as discussed in 74 2. The resource allocation problem in software applications A0, A9, B02, R1, R3, R43, R5, R6, R7, R8, R103, R11, R13, R14 A02, B02, R1, R2, R3, R43, R5, R6, R7, R8, R9, R103, R11, R12, R13, R14 T12 A02, B1, B11, R1, R3, R43, R5, R6, R7, R9, R103, R11, R13, R14 A0, A1, B02, R1, R3, R42, R5, R6, R7, R8, R102, R11, R12, R13 A02, B0, B1, R1, R2, R3, R42, R5, R6, R7, R9, R102, R11, R13, R14 T1 T13 T11 T26 A0, A2, B02, R3, R42, R6, R7, R8, R9, R102, R11, R12, R13, R14 T2 A0, A1, B0, B1, R1, R3, R4, R5, R6, R7, R10, R11, R13 T13 A0, A8, B02, R3, R42, R5, R6, R9, R102, R11, R12, R13, R14 T3 T4 T5 T6 T7 A02, B0, B10, R1, R2, R3, R42, R5, R6, R8, R102, R11, R14 T10 T25 T14 T1 A0, A6, B0, B1, R2, R42, R6, R7, R9, R11, R13, R14 A0, A6, B0, B11, R43, R6, R7, R9, R10, R11, R13, R14 A1, A6, B02, R42, R6, R7, R8, R11, R12, R13 A6, A9, B03, R42, R6, R7, R8, R10, R11, R13, R14 T1 T11 T12 T26 T13 T27 T8 T9 A0, A2, B0, B1, R3, R4, R6, R7, R9, R10, R11, R13, R14 T13 T2 T13 T3 A0, A2, B0, B10, R3, R4, R6, R8, R10, R11, R14 T25 A0, A3, B0, B10, R3, R4, R5, R8, R10, R11, R14 T3 T25 A0, A4, B0, B1, R3, R4, R5, R6, R9, R10, R11, R13, R14 T13 T4 A0, A3, B0, B2, R3, R4, R7, R8, R9, R10, R11, R14 T14 T14 T4 A0, A4, B0, B3, R3, R4, R5, R8, R9, R10, R11, R14 T15 A0, A5, B0, B3, R3, R4, R7, R9, R10, R11, R14 A0, A6, B0, B3, R2, R42, R7, R8, R9, R11, R14 T5 T16 T7 T6 T16 A0, A7, B0, B4, R3, R4, R5, R8, R9, R10 T8 T17 T18 T6 T7 T6 A0, A2, B0, B9, R4, R7, R8, R9, R10, R11, R14 T24 A6, A9, B0, B5, R4, R6, R8, R10, R14 A0, A3, B02, R3, R42, R5, R7, R8, R9, R102, R11, R12, R13, R14 A0, A3, B0, B1, R3, R4, R5, R7, R9, R10, R11, R13, R14 A0, A6, B1, B5, R2, R6, R9, R14 A0, A6, B5, B11, R4, R6, R9, R10, R14 T13 T11 T27 T26 T7 T1 T12 A0, A7, B0, B6, R4, R7, R8, R10, R14 T19 A0, A8, B0, B6, R4, R6, R10, R11, R14 T9 A0, A8, B0, B7, R3, R4, R5, R10, R11, R14 A0, A8, B0, B8, R3, R5, R9, R102, R12, R14 A0, A8, B0, B9, R4, R5, R9, R10, R11, R14 A0, A1, B0, B9, R1, R4, R5, R7, R8, R10, R11 T21 T20 T23 T10 T22 A02, B0, B2, R1, R2, R3, R42, R6, R7, R8, R9, R102, R11, R14 A0, A1, B0, B2, R1, R3, R4, R6, R7, R8, R10, R11 T14 T15 T1 T15 A0, A8, B0, B2, R3, R4, R6, R9, R10, R11, R14 T10 T10 A02, B0, B4, R1, R2, R3, R42, R5, R6, R8, R9, R102, R11 T16 A0, A2, B0, B3, R3, R4, R7, R8, R9, R10, R11, R14 T2 T16 T17 T18 A0, A3, B0, B4, R3, R4, R5, R8, R9, R10, R11 T3 T17 T18 A0, A1, B0, B5, R1, R3, R5, R6, R8, R102, R12 T1 T2 A02, B1, B5, R1, R2, R3, R5, R6, R9, R102, R14 A02, B5, B11, R1, R3, R4, R5, R6, R9, R103, R14 T11 T12 T13 T26 T27 A02, B0, B6, R1, R2, R42, R6, R7, R8, R102, R11, R14 T19 A02, B0, B7, R1, R2, R3, R42, R5, R7, R8, R102, R11, R14 A02, B0, B8, R1, R2, R3, R4, R5, R7, R8, R9, R103, R12, R14 A0, A1, B0, B8, R1, R3, R5, R7, R8, R102, R11 A0, A9, B0, B8, R1, R3, R4, R5, R7, R8, R103, R14 A02, B0, B9, R1, R2, R42, R5, R7, R8, R9, R102, R11, R14 A02, B8, B11, R1, R3, R4, R5, R7, R8, R103, R14 T2 T1 T13 T20 T21 T1 T11 T12 T24 T13 T26 T27 T17 T3 T18 A0, A3, B0, B6, R4, R7, R8, R10, R11, R14 T19 T4 A0, A4, B0, B9, R4, R5, R8, R9, R10, R11, R14 T20 T23 A0, A5, B0, B9, R4, R7, R9, R10, R11, R14 A0, A5, B0, B10, R3, R4, R6, R10, R11, R14 T5 T8 A0, A5, B0, B8, R3, R7, R9, R102, R12, R14 A0, A7, B0, B1, R3, R4, R5, R7, R9, R10, R13, R14 T25 A0, A7, B0, B2, R3, R4, R7, R8, R9, R10, R14 T14 T9 T5 T6 T21 T21 T7 T22 T22 T7 T23 T6 A1, A6, B0, B8, R7, R8, R12 A0, A6, B1, B8, R2, R7, R9, R14 T12 T11 T13 T26 T27 T27 A0, A5, B02, R3, R42, R6, R7, R9, R102, R11, R12, R13, R14 A02, B0, B5, R1, R2, R3, R4, R5, R6, R8, R9, R103, R12, R14 A0, A9, B0, B5, R1, R3, R4, R5, R6, R8, R103, R14 T22 T23 A02, B1, B8, R1, R2, R3, R5, R7, R9, R102, R14 A0, A6, B02, R2, R43, R6, R7, R8, R9, R10, R11, R12, R13, R14 A0, A4, B02, R3, R42, R5, R6, R8, R9, R102, R11, R12, R13, R14 A0, A4, B0, B2, R3, R4, R6, R8, R9, R10, R11, R14 A0, A5, B0, B4, R3, R6, R9, R10, R11 T17 T18 A0, A6, B0, B5, R2, R4, R6, R8, R9, R10, R12, R14 A0, A6, B0, B4, R2, R42, R6, R8, R9, R11 A0, A5, B0, B5, R3, R6, R9, R102, R12, R14 A0, A7, B02, R3, R42, R5, R6, R9, R102, R11, R12, R13, R14 A1, A6, B0, B5, R6, R8, R12 A0, A8, B0, B3, R3, R4, R5, R9, R10, R11, R14 A0, A2, B0, B5, R3, R6, R8, R9, R102, R12, R14 A0, A2, B0, B4, R3, R4, R6, R8, R9, R10, R11 A0, A4, B0, B6, R4, R6, R8, R10, R11, R14 T21 A0, A3, B0, B5, R3, R5, R8, R9, R102, R12, R14 T22 A0, A4, B0, B8, R3, R5, R8, R9, R102, R12, R14 A0, A4, B0, B7, R3, R4, R5, R8, R10, R11, R14 A0, A5, B0, B7, R3, R4, R7, R10, R11, R14 A0, A6, B0, B7, R2, R42, R7, R8, R11, R14 A0, A6, B0, B8, R2, R4, R7, R8, R9, R10, R12, R14 A6, A9, B0, B8, R4, R7, R8, R10, R14 T1 T24 A0, A6, B8, B11, R4, R7, R9, R10 A0, A7, B0, B10, R3, R4, R5, R8, R10, R14 T1 A0, A1, B0, B3, R1, R3, R4, R5, R7, R8, R10, R11 A02, B0, B3, R1, R2, R3, R42, R5, R7, R8, R9, R102, R11, R14 Figure 2.17: Reachability graph of the net system in Fig. 2.16. The net has two livelocks. Markings are coloured depending on the strongly connected component they belong to. The initial marking is stressed with a thicker border around it 2.4. A cross-sectional view on the liveness analysis problem 75 B0 R1 T1 T2 T3 A1 A2 T4 T5 T6 B2 B1 R3 A0 R2 A0, B0, R2 T1 A1, B0, R1 A1, B1, R3A2, B1, R2 A2, B2, R1 A0, B2, R3 T4 T2 T5 T3 T6 Figure 2.18: Live and reversible PC2R net system with a 0-acceptable initial marking such that no minimal t-semiflow is ever realisable Subsection 2.4.1). Both properties (reversibility and t-semiflow realisability) together imply that the net is live, as the next theorem states. Theorem 2.42. Let hN ,m0ibe a PC2Rnet system with a 0-acceptable initial marking. If the net system is reversible and every (minimal) t-semiflow xis eventually realisable (i.e., there exist m∈RS(N,m0), σ such that mσ −→,σ=x) then the net is live. Proof. By reduction to absurd: assume that the net is non-live. Then there exists m∈RS(N,m0) and a transition tsuch that tis dead at m. But since the net is reversible, there exists a sequence σsuch that mσ −→m0. Since the net is consistent by Lemma 2.22, there exists a t-semiflow xthat contains t, and xis eventually realisable, so tis eventually firable from a successor marking of m. But then tcannot be dead, reaching a contradiction. Nevertheless, it is notorious that those properties are almost unlinked for general PC2Rnet systems, with the exception of the rule established by Theorem 2.42. Table 2.1 illustrates in a concise way the relation between these three properties (liveness, reversibility, and eventual firability of all t-semiflows) in the context of general PC2Rnet systems with 0-acceptable initial markings. The table highlights the fact that those properties are not totally independent because of PC2Rnets being consistent, as proved by Theorem 2.42. It also reveals that the simpler the subclass, the less combinations of the three properties are possible (up to the point that liveness is a necessary and sufficient condition for reversibility for S4PR and simpler subclasses). Figure 2.21, which has not been introduced before, is used to complete the table. 76 2. The resource allocation problem in software applications L R T L R T L R T From L-S3PR upwards PC2R only From S5PR upwards Fig. 2.12 with K0= K1= K3= 1 Fig. 2.18 Figs. 2.16 and 2.17 L R T L R T L R T PC2R only IMPOSSIBLE PC2R only Fig. 2.9 Theorem 2.42 Fig. 2.8 L R T L R T From L-S3PR upwards PC2R only Fig. 2.12 with K0= K1= 1 and K3= 2 Fig. 2.21 Table 2.1: Summary of possible combinations of liveness (L), reversibility (R), and eventual realisability of every t-semiflow (T) for PC2R net systems with a 0-acceptable initial marking. For each cell, the first line indicates which (sub)class such properties combination is possible from. The second line references a proof of such behaviour Since, by Theorem 2.31, 1-acceptable initial markings grant the firability of every t-semiflow, a new corollary can be extracted from Theorem 2.42: Corollary 2.43. Let hN,m0ibe a PC2Rnet system with an 1-acceptable initial marking. By Theorem 2.31, if the net system is reversible then it is also live. Once more, it should be stressed that the reverse of Corollary 2.43 does not hold in general, as Figs. 2.16 and 2.17 prove. The same thing applies for the PC2Rnet in Fig. 2.19. Note that this net only has one single elementary iteration block per process subnet (i.e., no internal loops). The reachability graph is depicted in Fig. 2.20. Table 2.2 synthesises the relation between liveness and reversibility in general PC2Rnet systems with 1-acceptable initial markings. 2.5 An insight on the problem of RASs with lender processes Finally, it is worth bringing to attention the existence of yet another class of Petri net models for RASs, named SPQR [LGC06]. This class is interesting from the point of view of RAS analysis and synthesis in the domain of multithreaded programming. In the following subsections, this is made obvious since it is tightly related to the PC2R class. As a class on its own, SPQR nets feature an appealing syntactic simplicity and 2.5. An insight on the problem of RASs with lender processes 83 3. For each i∈INthe subnet generated by restricting Nto hPi, Tiiis a connected acyclic state machine. This is called the i-th process subnet. 4. For each r∈PR, there exists a unique p-flow yr∈ZZ|P|such that {r}= kyrk ∩ PR,kyrk ∩ PS6=∅, and yr[r] = 1. The reader can easily check that the composition of a non-empty set of PLPs by fusion of the common resource places is always an SPQR net, assuming that the various sets Pi(Ti) are disjoint. Equivalently, any SPQR net can be seen as the composition of a non-empty set of PLPs by fusion of some shared resource places. The concept of holder and lender places will be frequently used in the following. Aholder place is a process place in which processes use one or several instances of a type of resource r, i.e. {p∈Pi|yr[p]>0}. As PLPs can have non-positive p-flows, it is necessary to introduce a new concept: lender places. Definition 2.46. [LGC06] Let Nbe a PLP,p∈PS, and r∈PR: •pis a holder place of riff yr[p]>0. The set of holders of ris denoted Hr. •pis a lender place of r, iff yr[p]<0. The set of lenders of ris denoted Lr. The term lender process refers to a process subnet which contains at least one lender place of some resource. Conversely, the term borrower process refers to a process subnet which does not contain any lender place of any resource. For historical reasons, a particular subclass of SPQR, called borrower SPQR (bSPQR), is identified in the following: Definition 2.47. [LGC06] A borrower SPQR (b-SPQR) net is an SPQR net such that, for every r∈PR, the p-flow yr(see point 4 in Definition 2.45) is a minimal p-semiflow, i.e., yr∈IN|P|. In other words, a b-SPQR net is an SPQR net without lender processes. Note that any S4PR or S3PR net belongs to the b-SPQR class, taking its idle places as resource places. A significant subclass of b-SPQR is the subclass of Open L-S3PR [GV99]. 2.5.3 The SPQR class: Some structural properties In this subsection, we present a review of some structural properties of the SPQR class, with a special focus on properties which are relevant to liveness analysis. Some of these properties are yet unseen within the family of well-known Petri net models for analysing RASs. As a contrast to the PC2Rclass, for instance, it is revealed that SPQR nets are not, in general, Structurally Live (SL). In the last part of the subsection, it is formally proved that the process subnets of b-SPQR nets hold that ‘acquire’ operations always precede ‘release’ operations. 84 2. The resource allocation problem in software applications Conservativeness and consistency First it will proved that SPQR nets are consistent: Proposition 2.48. SPQR nets are consistent, i.e. ∃x>0s.t. C·x=0. Proof. Acyclic state machines are consistent. Therefore, ∃x>0 s.t. C[PS, T]·x= 0. It will be proved now that C[PR, T]·x= 0. For each r∈PR,C[r, t] = −yr[PS]· C[PS, T] by point 4 in Definition 2.45. Thus, for each r∈PR,C[r, t]·x=−yr[PS]· C[PS, T]·x= 0. Corollary 2.49. The set of t-semiflows of an SPQR net is equal to the union of t-semiflows of each process subnet (which are acyclic state machines). A well-known general result of Petri nets is that conservative nets are SB [SC88]. However, the inverse may not be true. In SPQR nets, nonetheless, conservativeness and structurally boundedness are equivalent. This is due to the fact that SPQRs nets are consistent by construction, and consistency plus SB implies conservativeness [Sil93]. Consequently, the acronym SB SPQR (or SB b-SPQR) denotes the subclass of nets in which every place of the net is covered by a p-semiflow. Structural Boundedness and Structural Liveness It can be inferred from the above discussion that an SPQR net Nis SB iff every process place is SB. A process place is SB only if it is holder of at least one resource place, but this condition is only necessary, not sufficient, e.g., in Fig. 2.22.c), place E is a holder place of R5, while place F is a holder place of R6. However, both places E and F are unbounded if R5 or R6 are initially marked (i.e., non-empty). Note that R5 and R6 are SB. This result differs from S4PR nets, in which every net of the class is conservative (and hence SB). Another interesting difference is that resource places are no longer structurally implicit places. In the S4PR class, this property was derived from the fact that every place was covered by a p-semiflow yrplus the existence of the idle place, which induced an additional p-semiflow which covered every process place. Here both conditions disappear. As a consequence, SPQR nets are not, in general, SL; even despite they are always consistent. S4PR nets were SL because every resource place could be made implicit taking an initial marking higher enough. Doing so, the system became a set of isolated marked strongly connected state machines, hence being live. However, even some very simple SB b-SPQR nets are not structurally live, as the Open L-S3PR [GV99] in Fig. 2.22.b) proves. Regardless of the initial marking, this net can always be deadlocked by emptying places C2 and D2 by firing transitions T9 and T12 as many times as possible, and subsequently emptying R3 and R4 by repeatedly firing 2.5. An insight on the problem of RASs with lender processes 85 c) R2 R1 T1 T2 T3 A1 A2 T6 T5 T4 B1 B2 R4 R3 T7 T8 T9 C1 C2 T12 T11 T10 D1 D2 R6 R5 T13 E T14 T16 F T15 2 a) b) Figure 2.22:a) Non-live SB SPQR net system with one lender process on the left, and one borrower process on the right. b) Open L-S3PR (therefore, SB b-SPQR net) which is not structurally live, i.e., it is non-live for every possible initial marking. c) SPQR net with two lender processes. The net is not SB (places E and F are unbounded iff m0[R5]+m0[R6] 6= 0) transitions T7 and T10. This scenario raises interesting questions regarding liveness synthesis that, in some subclasses, are yet to be fully addressed. Structural Directedness The Structural Directedness (SD) property [TS93] states that for every pair of potentially reachable markings of a live system there is always a common successor marking. SD is, indeed, a stronger, structural version of the directedness property [BV84], which will be studied among the behavioural properties, and holds for classes such as Equal Conflict (EQ) systems [TS93]. SD is very interesting from the standpoint of liveness analysis since it implies the absence of killing spurious solutions or, in other words, of live systems with potentially reachable markings being non-live. It has been proven that SD is satisfied for the L-S3PR class [GV99], but unfortunately it is not for any other known superclass, including the S3PR class. The lack of this property hardens liveness analysis, due to the emergence of killing spurious solutions, and is obviously extensible to the more general SPQR class; although the reachability space of live SB SPQR net systems is not always directed either, as shown in Fig. 2.9 and discussed later. On the processes structure Finally, it will be shown how b-SPQR nets differ from general SPQR nets in the way their processes are constructed: nets belonging to that subclass can be identified at a glance. Since each process subnet is an acyclic state machine, a partial order can be established for its set of transitions. The operator ¹will serve the purpose. 86 2. The resource allocation problem in software applications Definition 2.50. Let N=hPS∪PR, T, Cibe an SPQR net. We define ¹as a binary relation in Tsuch that t1¹t2(t1precedes t2) iff exists a directed path from t1to t2 in a process subnet or, in other words, in the subnet generated by PS, T. Further technical details on this operator are provided in a previous work of ours [LGC06]. For notational convenience, t1≺t2denotes t1¹t2and t16=t2. The following corollary establishes the relation between t-semiflows and the new precedence operator. Corollary 2.51. By Corollary 2.49, for every pair t1, t2∈Texists a minimal tsemiflow xsuch that t1, t2∈ kxkiff t1¹t2or t2¹t1. The precedence operator will now prove very handy to show how resources are used in b-SPQR nets. In these nets, transitions that take tokens from PRalways precede those that put tokens into PR, in such a way that every resource instance has been borrowed before than released. In other words, resources are always used in an acquire-before-release basis. This is a corollary of the following proposition: Proposition 2.52. Let xbe a minimal t-semiflow of an SPQR net with no lender places in the t-component induced by x. Then, for every u∈ kxk,C[PR, T ]·1τ≤0, where τ={t∈ kxk | t¹u}. In other words, the sum of weights of the incoming arcs from PRto the ‘prefix’ τ, is above or equal to that of the outgoing arcs. Proof. Let ¯τ=kxk \ τ, and let Pxbe the set of process places in the t-semiflow induced by x, i.e. Px= (•kxk∪kxk•)∩PS. By point 4 in Definition 2.45, for every r∈PR,C[r, T ] + yr[PS]·C[PS, T] = 0. If both terms are multiplied by 1τ, it is obtained: C[r, T]·1τ+yr[Px]·C[Px, T]·1τ= 0 (note that PShas been replaced by Pxdue to the fact that C[p, ¯τ] = 0for every p∈PS\Px). Taking into account that, by Corollaries 2.49 and 2.51, the subnet generated by Pxand kxkis a directed path of a process subnet (from a trigger to a drain transition), and ¯τis the set of transitions of a suffix of that directed path, then C[Px, T]·1τ≤0. Since there are no lender places in Px,yr[Px]≥0and then C[PR, T]·1τ≥0. By Corollary 2.49,C[PS, T]·x=0. Since C·x=0, then C[PR, T]·x=0. Also by Corollary 2.49,x=1kxk=1τ+1τ. Thus C[PR, T ]·1τ=−C[PR, T]·1τ≤0. Corollary 2.53. b-SPQR nets do not have lender places. Thus, every ‘prefix’ τof a minimal t-semiflow holds C[PR, T]·1τ≤0; therefore it can be said that resources are always used in an acquire-before-release basis. 2.5.4 The SPQR class: Some behavioural properties Having presented some basic structural properties of the class, we address on the following a review of relevant behavioural properties regarding liveness. Some of the 2.5. An insight on the problem of RASs with lender processes 87 findings are shared with the PC2Rclass, although they are still somewhat surprising in a class of such syntactical simplicity (for instance, SPQR net systems do not hold the directedness property). The conclusion is that finding efficient liveness analysis methods for SPQR nets is presumably much harder than for previous classes such as the S4PR class. Liveness vs. deadlock-freeness One of the characteristic properties of the SnPR family (including the L-S3PR class) is that deadlock-freeness does not imply liveness [GV99]. In this sense, they are trickier than other well-known Petri net classes such as strongly connected free choice systems [Hil85], bounded strongly connected EQ systems [TS93] or CSS [LT79], where both properties are equivalent. On the contrary, liveness is not even monotonic with respect to the initial marking (neither to the marking of the process places, nor that of the resource places), with the L-S3PR as the unique exception [GV99]. In fact, for S3PR and S4PR nets, there is a discontinuity zone between the point where the resource places are empty enough so that no transition is ever firable (all the lower markings imply a deadlock), and the point where every resource place is implicit (higher markings in them imply liveness). The markings within these bounds switch discontinuously between liveness and nonliveness. Of course, the location of those points also depends on the marking of the process places. However, SPQR and b-SPQR nets are not (in general) SL, not even being SB, and this implies that there may no longer exist an upper liveness region (e.g., the net in Fig. 2.22.b). Reversibility and directedness In an S4PR net system with an acceptable initial marking, reversibility is a necessary and sufficient condition for liveness [Rev03]. However, the class considered here (SPQR) is more general so, in particular, reversibility is not necessary for liveness. Figure 2.9 depicts an SB SPQR net system which is live but not reversible. Besides, reversibility is neither sufficient for liveness, provided that it is no longer required that all the t-components are firable in isolation from m0. The directedness property [BV84] states that, for every pair of reachable markings in a live system, there is always a common successor marking. Although the directedness property obviously holds for the S4PR class (reversibility is a necessary and sufficient condition for liveness), it is not verified, in general, for the SPQR class, as once more Fig. 2.9 reflects. The reachability space of the net has two terminal strongly connected components, being the net live. For bounded marked nets, the directedness property is equivalent to the existence of home states [BV84]. Hence, live S4PR net systems have home states; indeed, 88 2. The resource allocation problem in software applications every reachable marking is a home state, including the initial marking m0, since the net is reversible2. This is very useful for determining if the net is non-live, since the death of the system can be reduced to: “Is m0unreachable from some reachable marking?”. Even more, if it is reachable, a path that leads to m0can be systematically constructed, and the length of this path is not higher than the size of the net, due to the structure of the S4PR class. The “bad” news here is that, since the directness property is not held by the SPQR class, not even if the net is SB, it cannot be inferred (in general) that a home state will exist, whether the net is live or not. Again, Fig. 2.9 is a good example of this kind of behaviour. This is a severe problem for determining non-liveness in an efficient way. 2.5.5 Transformations and class relations The SPQR class was defined as a general framework in which the philosophy and results on previous RAS subclasses could be deployed while providing some innovative elements for modelling much more complex systems [LGC06]. This includes all the necessary elements for modelling RASs in multithreaded software systems in similar terms to the definition of the PC2Rclass. However, two important remarks are in place. First, the modelling power of general SPQR nets is high enough (unboundedness, etc.) so as to make liveness analysis a very difficult task in the general case. Therefore, common sense dictates that simpler subclasses must be identified in order to succeed in finding structural liveness characterisations. Second, SPQR nets are somewhat ‘raw’ models. Remarkably, their process subnets are acyclic state machines, while software threads can have internal iterations in which resources are allocated or released, as discussed in Sect. 2.3. In fact, these models are not thought as the optimum target for a first abstraction of software systems into Petri net models. However, PC2Rnets or simpler models can be transformed or even directly mapped into the framework of the SPQR class. Once a model has been ported into the transformed space, the appealing syntax simplicity of SPQR nets can be helpful from a theoretical point of view in order to explore whether the system is live or not, and why. Somehow, they can work very well as ‘low-level’ models. Obviously, this requires that an appropriate subclass has been defined so that the focus is on an workspace equivalent to that of the original class, not on that of a more general class of systems. In this subsection we relate PC2Rnets and other subclasses of the SnPR family with those subclasses of the SPQR framework, and describe precise net transformation rules to travel from one to each other. 2It is interesting to note that, in live L-S3PR net systems, a stronger condition holds: every potentially reachable marking is a home state [GV99]. 2.5. An insight on the problem of RASs with lender processes 89 Lemma 2.54. Let N=hP0∪PS∪PR, T, Cibe an S4PR net [Tri03]. Then N0= hPS∪P0 R, T, Ci, where P0 R=P0∪PR, is an SB b-SPQR net. Proof. Let Ni,i∈IN, be the i-th process subnet in N[Tri03]. The subnet generated by restricting Nito hPi, Tiiis a connected acyclic state machine, since by Definition 1.1, condition 3, every cycle contains the idle place p0i. Note that this idle place is not removed, but ‘moved’ to P0 R. Moreover, there exists a unique p-semiflow y0i, ky0ik=Pi∪ {p0i}. Since p0i∈P0 Rand Pi∩P0 R=∅,y0iholds the condition 4 in Definition 2.45. Hence every process subnet in Nis a borrower process in N0, and N0 is a b-SPQR net. Since Nis SB by construction, then N0is an SB b-SPQR net. However, the inverse of Proposition 2.54 is not strictly true: not every SB b-SPQR net is an S4PR net. However, any SB b-SPQR net can be easily transformed into an S4PR net by introducing a structural implicit place per process subnet connecting its drain transitions (transitions without output process places) with its trigger transitions (transitions without input process places). Obviously, the initial marking of this place (the new idle place) must be made high enough so as to make the place implicit. Fortunately, this can be accomplished thanks to the fact that the original net is SB. Obviously, S3PR [ECM95] and L-S3PR [EGVC98] nets can be also redefined as SB b-SPQRs nets, since they are children of the S4PR class. Similar redefinitions in terms of the SPQR class can be applied to any previously defined Petri net model for Sequential RASs, except for S*PR nets, since the SPQR class does not directly deal with internal cycles. Note that all the above transformations are presented for completion (i.e., as a proof that previous subclasses can be easily mapped into the new framework), although they have no interest from a practical point of view. On the other hand, transforming PC2Rnets into SPQR nets can make much sense for the aforementioned reasons. Significantly, it is always possible to transform aPC2Rnet system into an equivalent SB SPQR net system, preserving its behaviour with relation to liveness (indeed, the language of firing sequences is equivalent in the transformed net system). The transformation rule is based on the idea of converting every while-do block into an acyclic process which is activated by a lender resource place. This lender place gets marked once the thread reaches the while-do block. The token is removed at the exit of the iteration. This transformation must be applied from the innermost loops outwards. Figure 2.23 depicts the transformation rule. The rule preserves the language accepted by the net (and thus liveness) since it basically consists in the addition of a implicit place (place P1 in the right hand net of Fig. 2.23, since R P1 can be seen as a renaming of P1 in the left hand net). Figure 2.24 illustrates the transformation of the PC2Rnet system in Fig. 2.13 into the corresponding SB SPQR net system. 90 2. The resource allocation problem in software applications P2 T5T5 T1 T3 T4 T3 T4 PR R_P1P1P1 P3 P3 T2 T6 T2 T6 P2 T1 Figure 2.23: Transforming PC2R into SB SPQR nets: From iterative to acyclic processes Structurally speaking, it is also possible to transform an SB SPQR net into a PC2R net. In the same vein than for S4PR nets, it is just necessary to add a structural implicit place per process subnet connecting its drain transitions with its trigger transitions, which will be the idle place of the process subnet of the resulting PC2R net. Out of curiosity, the concept of acceptable initial marking has not been defined for the SPQR class, since it was conceived as a model to support generalised FMSs which support warm booting or where the processes are open plans. On the other hand, the concept of (0/1-) acceptable initial marking does have a physical meaning in the context of PC2Rnets modelling real-world systems in software engineering. As a lateral effect, the transformation of an SB SPQR net system hN ,m0iinto a PC2Rnet system hN0,m00imay not produce a net system with a 0-acceptable initial marking m00, even when m0[PS] = 0. 2.6 Conclusions Although there exist a variety of Petri net classes for RASs, many of these definition efforts have been directed to obtain powerful theoretical results for the analysis and synthesis of this kind of systems. Nevertheless, the process of abstraction is a central issue in order to have useful models from a real-world point of view, and therefore requires careful attention. In this chapter, that path has been followed, constructing a list of requirements for obtaining an interesting Petri net subclass of RAS models applied to the software engineering domain. Considering that list, the class of PC2R nets has been defined. It fulfils those requirements while respecting the design philosophy on the RAS view of systems. Some useful transformation and class relations have also been introduced so as to locate the new class among the myriad of previous models. 2.6. Conclusions 91 TA8 TB3TB4TB5 B2B4 B3 TA2 TA3 TA5TA4 TB8 A2 FORK1 FORK2 BOWL R_A1 R_B1 TA7 TA6 A0 TB7 TB6 B1 B6 B0 B5 A1 A5 A6 TA1 TB1 A3 A4 TB2 A0, B0, FORK1, FORK2, BOWL A1, B0, FORK2, BOWL, R_A1 TA1 A0, B1, FORK1, BOWL, R_B1 TB1 A5, B0 A6, B0, BOWL TA8 TA7 TA6 A0, B5 A0, B6, BOWL TB8 TB7 TB6 A1, B1, BOWL, R_A1, R_B1 TB1 TA1 A1, A2, B0, FORK2 A0, B1, B2, FORK1 TB2 A1, A2, B1, R_B1 TA2 A1, B1, B2, R_A1 TB2 A1, A4, B1, R_B1 A1, B1, B4, R_A1 TA4 TB4 TA5 TB5 A1, A3, B1, R_B1, FORK1 A1, B1, B3, R_A1, FORK2 TA3 TB3 TA2 TA5 A1, A3, B0, FORK1, FORK2 A1, A4, B0, FORK2 TA3 TA4 TB1 TB1 TB1 TB5 A0, B1, B3, FORK1, FORK2 A0, B1, B4, FORK1 TB3 TA1 TA1 TA1 TB4 Figure 2.24: From PC2R to SB SPQR nets: Two postmodern dining philosophers Furthermore, it has hopefully been proved that the problem of liveness in the new context is non-trivial and presented some cases of bad behaviour. In some cases, the results are surprising and clearly reveal the inherent complexity of the class. Remarkably, it is revealed that the previous siphon-based characterisations for liveness analysis are no longer valid in this domain. Finally, a Petri net class called SPQR has been introduced for modelling a very general category of Sequential RASs. This allows to model abstractions of FMSs where the number of processes following the process plans is not limited and these processes can have already allocated resources 92 2. The resource allocation problem in software applications Property L-S3PR S3PR S4PR S5PR PC2R [1] PC2R [2] SPQR Structural Well-formedness X X X X X X × Struct. directedness X× × × × × × Behavioural (for an m0acceptable for the class) RS = PRS 3× × × × × × × Deadlock-free = Live × × × × × × × Liveness monotonicity X× × × × × × Directedness X X X × × × × Reversible =⇒Live X X X X X × × Realisable t-semiflows X X X X X × × Table 2.3: Comparison of some basic structural and behavioural properties related to liveness. All behavioural properties are presented for net systems with acceptable initial markings, except for [1] (1-acceptable) and [2] (0-acceptable). from the start. The new SPQR framework colligates previous models and theoretical achievements for dealing with the RAP. Additionally, the generalisation is enriched providing support for other types of Sequential RASs which were not supported by previous classes. A subclass of SPQR has been identified which looks promising so as to provide a simple yet powerful theoretical framework in which study the liveness analysis problem for multithreaded software systems. To sum up, Table 2.3 highlights some similarities and differences between the different members of the SnPR family, while Fig. 2.25 introduces the inclusion relations between the Petri net classes for Sequential RASs which have been introduced so far. 3Reachability Set = Potentially Reachability Set. 3.2. On siphon-based liveness enforcing in FMSs 99 the siphons of the original net, but also those new siphons which appear when others are being controlled. Furthermore, this kind of techniques have a major handicap. Although the strategy of addition of monitors works fine for simple RASs classes, such as those that are structurally safe [GVTCE98], such approaches have deeper problems in more general circumstances. Not only happens that sometimes there does not exist a single place to cut a terminal strongly connected component in a complete and isolated way, but occasionally the elimination of one of its markings through a monitor place requires removing legal markings from other strongly connected components. This happens even for RAS classes whose net models are ordinary and their processes are linear, i.e., which lack on-line decisions [GV99]. Later in Subsection 3.2.2 we will see an example of this type of phenomenon. This circumstance is due to the fact that monitor places introduce linear marking constraints (i.e., the weighted sum of tokens in a set of places is limited by some number), while some of those unwanted markings may be trapped in the convex hull of the space of legal markings. This means that (to make a clean excision) we need a non-linear constraint that can cut this kind of markings. In this context, it has been proposed the introduction of disjunctive constraints through control mechanisms that are no longer a single place, but instead a subnet which overcomes the aforementioned obstacle [IA07]. A major difficulty in this kind of approaches is, again, the fact that the subnet introduced to control the siphon may leave the resulting Petri net out of the class of networks that can be analysed with the classic theory of siphons in RASs. Another common approach for liveness enforcing through the addition of monitors is based on the exploration and manipulation of the state space of the net, leaving aside siphons as a structural means of approaching non-liveness. In this context, it is essential that bad states are categorised, taking into account not only those in which there exist dead transitions, but also those markings which are doomed to deadlock. Nevertheless, the biggest obstacle that this kind of approaches manifest is to handle the state explosion problem, aggravated especially in highly concurrent RASs. Due to the computational complexity of dealing with the reachability set, the use of symbolic representations of sets of markings through Ordered Binary Decision Diagrams (OBDDs) has been proposed in order to obtain a compact representation of the set of forbidden markings [GVTCE98]. This ultimately allows the definition of a temporal logic and the efficient computation of the control logic (i.e., the set of monitors) through model checking techniques. A different subfamily of approaches on the problem relies on the Theory of Regions (or variations of it) to tackle the state explosion problem and the addition of monitors that forbid bad states [GRX03,UZ07]. Recent works address the classification of the reachability space through non-linear classifiers, tackling the problem of bad markings that become trapped in the convex hull of the space of legal markings [NR12]. 100 3. The liveness problem: Characterisation, analysis and synthesis A different set of techniques is based on the structure of the Petri net as a graph. Typically, they consider the relations among resources and they look for dangerous relations, as circular waiting relations among resources. The Petri net structure typically reflects the relations of use among resources (which are the main problem when dealing with deadlocks) and, in this sense, several approaches have been presented trying to exploit this. One of the most common approaches is based on the usage of digraphs [FZ04]. In this vein, railway networks originally modelled by means of coloured Petri nets have been approached by way of digraphs from a RAS perspective [FGS06]. The resulting control logic is incorporated to the original net system in the form of colored monitor places. The approaches based on the relation among bad states and structural components of the Petri net have their starting point in the seminal work of J. Ezpeleta, J-M. Colom and J. Mart´ınez [ECM95]. That paper presented a characterisation of the liveness problem in S3PR in terms of empty siphons. Many papers have later tried to either extend those results to more general classes of Petri nets or to explore them [Tri03,PR01,TGVCE05,HJXC06,Rev07,HZL11]. A first family of approaches to the problem of synthesising live FMSs from a structural perspective is based on the computation of all siphons that may be involved in a deadlock, in order to control them. In the context of S3PR nets, this often results in the need for algorithms for computing the set of minimal siphons since, for this kind of models, any deadlock situation is associated with at least one minimal empty siphon. This is essentially the approach originally presented in the aforementioned seminal work [ECM95]. Some work has been done later to avoid the computation of all minimal siphons, trying to reduce the computational complexity by only controlling a significant subset of them [LZ08]. The core of this kind of approaches is to try to obtain truly independent siphons by means of its interactions via transitions (dependency is measured by linear combinations of transitions related to the siphon). Other works try to avoid the computation of all minimal siphons through the introduction of hybrid strategies in which the state space of the net is also explored [PCF09]. The pruning graph [CRC12] is a powerful artifact that not only allows the computation of every minimal siphon in a S4PR net, but also provides a concise insight on how these siphons are constructed. For S3PR nets, minimal siphons are enough to characterise deadlock situations. The pruning graph will be further introduced in Subsection 3.2.3. An alternative route for structural control based on siphons passes through the introduction of iterative synthesis strategies based on the individual search of potentially dangerous siphons and their control through monitors. This scheme is repeated until a live system is obtained, which sometimes means avoiding the computation of a significant number of siphons. 3.2. On siphon-based liveness enforcing in FMSs 101 2 A0 B2 TA2 TA4TA1 TB1 TB2 A2 B1 B0 A1 TA3 A3 R2 R1 TB3 2 22 2 TA1 A1, B0, R12, R2 TB1 A1, B1, R1, R2 A2, B0, R2 A0, B2, R12 TB1 TA1 TA2 TB2 A3, B0, R12 TA3 TA4 TB3 A3, B2 TB3 TA4 A3, B1, R1 A0, B0, R12, R22 TB1 TA4 A0, B1, R1, R22 spurious marking Figure 3.1: A non-live S4PR net system to be controlled In this vein, several studies have appeared that address the computation of problematic siphons and monitor places through techniques based on ILP [Tri03, TGVCE05,HZL11]. In the next subsection we will discuss an approach based on this last family of techniques, which will be illustrated through examples. 3.2.2 Managing siphons for the computation of virtual resources Computing virtual resources through mathematical programming Fernando Tricas et al. [TGVCE05] present an iterative algorithm for deadlock prevention based on ILP which is reviewed on the following. This result is grounded on the structural characterisation already presented in Theorem 1.5 and deployed in the context of supervisory control of FMSs for the rather general class of S4PR nets. With the help of the net state equation, a set of Integer Linear Programming Problems (ILPPs) can be constructed which prevents the costly exploration of the state space. As far as we know, other works on ILP-based liveness enforcing depart from a similar strategy even though the objective function to be optimised may differ. To illustrate the algorithm, the S4PR net system in Fig. 3.1 (which was already introduced in Chap. 1as Fig. 1.4) will be used. In each iteration, this algorithm searches for a bad siphon and a potentially reachable marking under which the siphon is insufficiently marked. If found, a control place is suggested to prevent that siphon from ever becoming insufficiently marked. Such control place will be a virtual resource, in such a way that the resulting Petri net remains into the S4PR class. Thanks to this, a new iteration of the algorithm can be executed. The algorithm terminates as soon as there do not exist more siphons to be controlled, i.e., the system is live. 102 3. The liveness problem: Characterisation, analysis and synthesis Prior to the introduction of the algorithm and its related ILPPs, some basic notation must be established. In the following, for a given insufficiently marked siphon D,DR=D∩PRand yDR=Pr∈DRyr. Notice that yDRexpresses the total amount of resource units belonging to D(in fact, to DR) used by each active process in their process places. Also: Definition 3.1. [TGVCE05] Let hN,m0ibe an S4PR net system. Let Dbe a siphon of N. Then, ThD=kyDRk\Dis the set of thieves of D, i.e. the set of process places of the net that use resources of the siphon and do not belong to that siphon. The next system of restrictions relates the liveness characterisation introduced in Theorem 1.4 with the ILPPs which are used in the forthcoming algorithm. Essentially, the characterisation is reformulated into a set of linear restrictions given a reachable marking and a related bad siphon. Proposition 3.2. [TGVCE05] Let hN ,m0ibe an S4PR net system. The net is non-live if and only if there exist a siphon Dand a marking m∈RS(N,m0)such that the following set of inequalities has, at least, one solution:                                                m[PS]≥ \0-- ∃t∈T:tis m-p-e ∀t∈T\P0•:with {p}=•t∩PS, m[p]≥et-- et=0 :tis m-p-d et≥m[p] sb[p]-- et=1 :tis m-p-e ∀r∈DR,∀t∈r•\P0•:m[r] Pre[r,t]≥ert -- ert=0 :tis m-r-d by r ert ≥m[r]−Pre[r,t]+1 m0[r]−Pre[r,t]+1 -- ert=1 :tis m-r-e by r ∀r∈PR\DR,∀t∈r•\P0•:ert = 1 -- ert=1 :r /∈D ∀t∈T\P0•:Pr∈•t∩PRert <|•t∩PR|+ 1 −et et∈ {0,1} -- if tis m-p-e then tis m-r-d by DR ∀r∈DR,∀t∈r•\P0•:ert ∈ {0,1}. (3.1) where sb[p]denotes the structural bound of p[CS91] Note that m-p-e (m-p-d) stands for m-process-enabled (m-process-disabled) and m-r-e (m-r-d) stands for m-resource-enabled (m-resource-disabled). The following proposition introduces a set of additional restrictions on the system (3.1) that characterise the condition of siphon for the set of places whose respective variables vpequal zero (observe that, for notational simplicity, we use vpfor process places and vrfor resource places). Note that the minimality of the siphon is not 3.2. On siphon-based liveness enforcing in FMSs 103 required, which makes sense considering that no minimal siphon characterises liveness for the class of S4PR nets, as introduced in Sect. 2.4. Therefore, the new proposition captures the characterisation introduced in Theorem 2.33 with a system of linear inequalities. Proposition 3.3. [TGVCE05] Let hN ,m0ibe an S4PR net system. The net is non-live if and only if there exist a siphon Dand a marking m∈RS(N,m0)such that the following set of inequalities has a solution with D={p∈PS∪PR|vp= 0}:                                                                      ∀p∈P\P0,∀t∈•p:vp≥Pq∈•tvq− |•t|+ 1 -- Dis a siphon Pp∈P\P0vp<|P\P0|-- |D|>1 m[PS]≥ \0-- ∃t∈T:tis m-p-e ∀t∈T\P0•:with {p}=•t∩PS, m[p]≥et-- et=0 :tis m-p-d et≥m[p] sb[p]-- et=1 :tis m-p-e ∀r∈PR,∀t∈r•\P0•:m[r] Pre[r,t]+vr≥ert -- ert=0 :tis m-r-d by r and r∈D ert ≥m[r]−Pre[r,t]+1 m0[r]−Pre[r,t]+1 -- ert=1 :tis m-r-e by r ert ≥vr-- ert=1 :r /∈D ∀t∈T\P0•:Pr∈•t∩PRert <|•t∩PR|+ 1 −et-- if tis m-p-e then ∀p∈P\P0:vp∈ {0,1}tis m-r-d by DR ∀t∈T\P0•:et∈ {0,1} ∀r∈PR,∀t∈r•\P0•:ert ∈ {0,1}. (3.2) where sb[p]denotes the structural bound of p[CS91]. Note that m-p-e (m-p-d) stands for m-process-enabled (m-process-disabled) and m-r-e (m-r-d) stands for m-resource-enabled (m-resource-disabled). Thanks to the addition of the net state equation as another linear restriction, the following theorem constructs an ILPP which can compute a marking and a bad siphon holding System (3.2). Nevertheless, that marking can be a spurious solution of the state equation. Since this kind of nets can have killing spurious solutions (i.e, spurious solutions which are non-live when the original net system is live) then the theorem establishes a necessary but not sufficient condition. This is usually not a problem when the objective is to obtain a live system: the only consequence can be that some harmless, unnecessary control places are added. These control places would forbid some markings which are not really reachable. 104 3. The liveness problem: Characterisation, analysis and synthesis Since one siphon must be selected, the ILPP selects that with a minimal number of places, hoping that controlling the smallest siphons first may prevent controlling the bigger ones. Other works present analogous techniques with a different objective function for this ILPP [HZL11]. Theorem 3.4. [TGVCE05] Let hN ,m0ibe an S4PR net system. If the net is non-live, then there exist a siphon Dand a marking m∈PRS(N,m0)such that the following set of inequalities has, at least, one solution with D={p∈PS∪PR|vp= 0}: max Pp∈P\P0vp s.t. m=m0+C·σ m≥0,σ∈IN|T| System (3.2) The previous theorem can compute a marking mand a related bad siphon D. However, siphon Dcan be related with a high number of deadlocks, and not only with that represented with m. For that reason, the aim is to compute a control place able to cut every unwanted marking which the siphon Dis related to. Consequently, two different strategies are raised from the observation of the set of unwanted markings: (i) adding a place that introduces a lower bound of the number of available resources in the siphon for every reachable marking (D-resource-place), or (ii) adding a place that introduces an upper bound of the number of active processes which are withdrawing tokens from the siphon (D-control-place). In order to define the initial marking of such places, two constants must be computed which are the result of two ILPPs. These ILPPs evaluate every unwanted marking that a bad siphon is related to: Definition 3.5. [TGVCE05] Let hN ,m0ibe an S4PR net system. Let Dbe an insufficiently marked siphon, mmax Dand mmin Dare defined as follows, with vp= 0 iff p∈D: mmax D= max Pr∈DRm[r]mmin D= min Pp∈T hDm[p] s.t. m=m0+C·σs.t. m=m0+C·σ m≥0,σ∈IN|T|m≥0,σ∈IN|T| m[PS\ ThD] = 0 m[PS\ ThD] = 0 System (3.1) System (3.1) The next definition establishes the connectivity and the initial marking of the control place proposed for a given bad siphon D, both whether that place is a Dprocess-place or a D-resource place. 3.2. On siphon-based liveness enforcing in FMSs 105 Definition 3.6. [TGVCE05] Let hN ,m0ibe a non-live S4PR net system. Let Dbe an insufficiently marked siphon, and mmax Dand mmin Das in Definition 3.5. Then, the associated D-resource-place, pD, is defined by means of the addition of the following incidence matrix row and initial marking: CpD[pD, T] = −Pp∈ThDyDR[p]·C[p, T ], and mpD 0[pD] = m0[D]−(mmax D+ 1). The associated D-process-place, pD, is defined by means of the addition of the following incidence matrix row and initial marking: CpD[pD, T] = −Pp∈ThDC[p, T], and mpD 0[pD] = mmin D−1. Finally, we can state the algorithm that computes the control places for a given S4PR net system. In those cases in which a D-resource-place with an acceptable initial marking cannot be computed, the algorithm proposes the corresponding Dprocess-place, which always has an acceptable initial marking [TGVCE05]. Algorithm 3.1 [TGVCE05] Synthesis of live S4PR net systems 1. Compute an insufficiently marked siphon using the ILPP of Theorem 3.4. 2. Compute mmax D(Definition 3.5). (a) If the associated D-resource-place (Definition 3.6) has an acceptable initial marking according to Definition 1.2, then let pDbe that place, and go to step 3. (b) Else, compute mmin D(Definition 3.5). Let pDbe the associated D-processplace (Definition 3.6). 3. Add the control place pD. 4. Go to step 1, taking as input the partially controlled systems, until no insufficiently marked siphons exist. Theorem 3.7. [TGVCE05] Let hN ,m0ibe an S4PR net system. Algorithm 3.1 applied to hN ,m0iterminates. The resulting controlled system, hNC,mC 0i, is a live S4PR net system such that RS(NC,mC 0)⊆RS(N,m0). Let us now apply Algorithm 3.1 to the net depicted in Fig. 3.1. There exists one deadlock (m≡[A1,B1,R1,R2]) and two insufficiently marked siphons in m, D1={R1,R2,A3,B2}and D2=D1∪ {A2}. None of these is minimal. When applied step 1 of Algorithm 3.1, the ILPP of Theorem 3.4 returns D=D1, since D1 has less places than D2. In step 2, we compute mmax D=m[R1] + m[R2] = 2. Since the associated D-resource-place has not an acceptable initial marking (only one token in it is insufficient at m0), then we compute mmin D=m[A1] + m[A2] + m[B1] = 2. In step 3, we add the associated D-process-place pDto the net. And finally, we go 106 3. The liveness problem: Characterisation, analysis and synthesis 2 A0 B2 TA2 TA4TA1 TB1 TB2 A2 B1 B0 A1 TA3 A3 R2 TB3 2 2 2 2 R1pD TA1 A1, B0, R12, R2 TB1 A1, B1, R1, R2 A2, B0, R2 A0, B2, R12, pD XX TA2 TB2 A3, B0, R12, pD TA3 TA4 TB3 A3, B2, pD TB3 TA4 A3, B1, R1 A0, B0, R12, R22, pD TB1 TA4 A0, B1, R1, R22 spurious marking Figure 3.2: The controlled system after applying Algorithm 3.1 on the net in Fig. 3.1 back to step 1. But now the net is live and the ILPP of Theorem 3.4 has no solution, so the algorithm finishes after its first iteration. The resulting controlled system is depicted in Fig. 3.2. Limits on permissivity Nevertheless, these techniques have certain limitations. For general S4PR nets, adding extra monitors to cut ‘bad’ states off and enforce liveness may also entail the removal of some legal markings. This happens when some unwanted marking can be obtained by a linear combination of two reachable markings which are legal (i.e., those which are not doomed to deadlock, and therefore ideally should not be forbidden). Then the unwanted marking is trapped in the convex hull of the space of legal markings. That means that any additional linear constraint that could be added to effectively forbid that marking necessarily would involve removing some legal extreme points. In other words, any GMEC which eliminates the unwanted marking also requires removing some legal marking. This type of limitation has already been addressed from the standpoint of general Petri nets [GVTCE98]; in fact, the net in Fig. 3.3 is a variation of an illustrative example presented in that work. Hereinafter, we will address the correction of this net system by means of Algorithm 3.1. This net contains a unique (minimal) bad siphon D={R1,R2,A2,B2}which is insufficiently marked (in the sense derived from Theorem 1.5) at the following reachable markings: [A0,A1,B0,B1,R1,R2] ≡m1 [A12,B0,B1,R2] [A0,A1,B12,R1] 3.2. On siphon-based liveness enforcing in FMSs 107 2 2 R1 R2 T1 T3 T2 A1 A2 T6 T5 T4 B2 B1 B0 A0 2 2 T1 A0, A1, B02, R1, R22 T4 A0, A1, B0, B1, R1, R2 A0, A2, B0, B2 T6 T3 A02, B02, R12, R22 A02, B0, B1, R12, R2 spurious marking A0, A2, B02, R12A02, B0, B2, R22 T2 T5 T3 T6 T4 T1 A12, B02, R22A02, B12, R12 A12, B0, B1, R2 A0, A1, B12, R1 A12, B12 T1 T4 T4 T1 T4 T1 T1 T4 A1, A2, B02, R1 T2 T3 A02, B1, B2, R2 T5 T6 T1 T4 Figure 3.3: A non-live S4PR net system with a non-convex permissible marking space [A02,B02]≡m2 Indeed, the siphon Dis empty at m2, which is a deadlock. Note that the other three markings are doomed to deadlock, and therefore should be forbidden as well. When applied step 1 of Algorithm 3.1, the ILPP of Theorem 3.4 returns D. In step 2, we compute mmax D= 2 (this value is obtained because of m1). In step 3, we add the associated D-resource-place pDto the net. And finally, we go back to step 1. But now the net is live and the ILPP of Theorem 3.4 has no solution, so the algorithm terminates. The resulting controlled system is depicted in Fig. 3.4. As shown in Fig. 3.4, the proposed solution includes the addition of a resource place pDcutting the four unwelcome markings that are shaded in a different color in both figures. However, this place also forbids two additional markings which do not inevitably lead to deadlock: [A12,B02,R22] and [A02,B12,R12]. Note that m0is still reachable from those markings. This last observation might suggest that the new resource place is not the optimal so as to cut the unwanted states off. However, it is easy to check that the marking [A0,A1,B0,B1,R1,R2], which inevitably leads to deadlock, lies in a midpoint between the two legal markings which have been eliminated. Certainly: [A12,B02,R22] + [A02,B12,R12] 2= [A0,A1,B0,B1,R1,R2] Therefore, any linear constraint added to remove such marking inevitably requires the elimination of any of those two legal markings. This example also illustrates another limitation of these techniques: by adding linear constraints that merely inhibit reachable markings, and therefore possible firing sequences, the system concurrence is reduced. In many cases, this negatively affects the system performance. The proposed control logic depicted in Fig. 3.4 not only 108 3. The liveness problem: Characterisation, analysis and synthesis 2 2 R1 R2 T1 T3 T2 A1 A2 T6 T5 T4 B2 B1 B0 A0 2 2 p D T1 A0, A1, B02, R1, R22 T4 A0, A1, B0, B1, R1, R2 A0, A2, B0, B2, pD T6 T3 A02, B02, R12, R22, pD A02, B0, B1, R12, R2 spurious marking A0, A2, B02, R12, pDA02, B0, B2, R22, pD T2 T5 T3 T6 X X A12, B02, R22A02, B12, R12 A12, B0, B1, R2 A0, A1, B12, R1 A12, B12 X X X X X T1 XX A1, A2, B02, R1 X T3 A02, B1, B2, R2 X T6 T1 T4 Figure 3.4: The controlled system after applying Algorithm 3.1 on the net in Fig. 3.3 inhibits completely the possibility that a process of type A (left process subnet) and a process of type B (right process subnet) ever coexist in the system, but even the circumstances under which two processes of the same type concur are reduced. Non-redundant virtual resources Another possible undesired consequence of using this type of approach is that of obtaining a set of places wherein some of them may be redundant for the control of the net, in the sense that their removal would preserve the language of firing sequences of the net. In other words, some of the control places may be implicit places. As introduced in Lemma 2.27, every resource place of an S4PR net is structurally implicit. Therefore, every monitor place added to prevent a siphon from becoming insufficiently marked is also an SIP. This does not necessarily mean that these places are implicit, as this depends on their initial marking. In fact, usually the last resource place added with this type of iterative approach is not an implicit place. This is due to the fact that it must cut at least one bad marking that was allowed so far. Provided that at least one such marking is not a spurious marking we can state that the introduction of the monitor place restricts the language of firing sequences of the net, and thus the place is not implicit. However, the introduction of a new resource place, even not being implicit, can make redundant (i.e., implicit) some of the previously existing monitor places in the net [Tri03]. From the standpoint of the control engineer, this is an undesirable situation that can lead to the introduction of unnecessary control mechanisms involving a cost overrun or overcomplicate the system maintenance. For this reason, post-processing techniques should be applied to cut implicit places after obtaining the control logic. Despite the NP-completeness of determining, in the general case, the minimum initial marking that makes an SIP implicit [GVC99], there 3.2. On siphon-based liveness enforcing in FMSs 115 Another problem which was illustrated in Subsection 3.2.2 is that the strategy of adding linear restrictions through monitors to enforce liveness may inevitably imply that some legal behaviour is prevented from happening. This was already illustrated through the net in Fig. 3.3 and Fig. 3.4. Finally, the computation cost of computing all siphons that can be problematic so as to control them (and remove the redundant control logic) can be specially demanding for systems in which there exists a high number of types of resources. In the next subsection we present a different family of structural synthesis techniques which somehow transgress some of the principles of classic control theory but can provide a different category of solutions which can be complementary in certain scenarios. 3.2.4 Structural regions and the privatisation of resources Principles of the technique So far we have reviewed the structural synthesis methods directly derived from the characterisation of the liveness property. In this context the reason for the nonliveness appearing is in the bad siphons with a small number of tokens inside. The synthesis strategy consists of the control of the siphon in such a way that the number of tokens inside the siphon always is greater than or equal to a value guaranteeing the liveness of the transitions covered by the siphon. Therefore the basis of the strategy is a control-based strategy where we introduce extra constraints to the transitions allocating new copies of the resources of the siphon that prevent that the number of these copies go under a dangerous value. Given the iterative nature of the method, the constraints are constructed as new (virtual) resources of the system whose availability represents the constraints to the allocation of the original resources. This procedure allows us to maintain the net controlled in an intermediate iteration within the class of nets for which a siphon-based characterisation of the liveness property exists, and so we can proceed with the next iteration. We must point out here that these techniques adhere to some common rules or characteristics. The infringement of such rules gives rise to the new techniques introduced later in this section. The rules or characteristics shared by those techniques based on virtual resources are: •The controlled net respects the original state machines (the production plans) and the initial marking of the state machines (the initial marking of the idle places). For the designer, this means that the original system is completely maintained and so s/he can identify his/her original design. •The same happens with respect to the original resources of the net system. The controlled net contains the same resource types (resource places) as in the 116 3. The liveness problem: Characterisation, analysis and synthesis original net, and the initial marking of these resource places is the same (the number of copies of each type of original resource is maintained). •Liveness enforcing by means of virtual resources is based on the addition of some places that represent additional constraints to the transitions in charge of the allocation of some original resources when a request of a process (a token in a process place) arrives to the controller of the resource. The effect of these additional virtual resources is to forbid some occurrence sequences of transitions of the original net to prevent an excessive decay in the marking of a bad siphon. In other words, it is the classical approach inside control theory, where the goal is to forbid states or occurrence sequences. Therefore, the constraints reduce the concurrency inside the system because some occurrence sequences are forbidden and the resource utilisation rate is reduced because some states where resources are in use are forbidden. Observe that these three characteristics are shared by all techniques inspired in the use of siphons. Nevertheless, in this section, for a particular subclass of nets, we present a technique in which the three previous characteristics are not respected. That is, we propose a technique where the central point is the addition of copies of the original resources. It is well known that in bounded systems, if we are able to increase the number of copies of resources then all deadlock problems disappear because the resource places become implicit places and can be removed. Nevertheless, we try to add a minimum number of copies of resources because they can be expensive, then in order to minimise this we specialise the original copies of a type of resource in the sense that certain copies only can be used by a subset of processes and the other copies of resources are used only by the rest of processes. This idea will be implemented by splitting a type of resource (a resource place) into two new types of resources each one used in a private way by a a disjoint subset of processes of the original system. Therefore, we increase the number of copies of the original resources but increasing the degree of privatisation of the use (or, in other words, reducing the degree of resource sharing). We will see that this technique, from a structural point of view, breaks the original bad siphons, and then if we are able to break all bad siphons the net cannot have deadlocks. At our best knowledge, this is a completely novel strategy [Rov11]. The positive effect in the global behavior of the system is that concurrency is not reduced. In fact, all original states of the system remain reachable and new states are added representing the recovery states from the deadlocks to the safe states of the system. Therefore, these techniques are not based on the forbidden state strategy coming from control theory. In the following, the non-live S3PR net depicted in Fig. 3.9.a is used to illustrate the different techniques of liveness enforcing presented in this work and the different 3.2. On siphon-based liveness enforcing in FMSs 117 R2 R1' T5 T6 B1 B2 T1 T2 T3 T4 A0 A1 A2 B0 R1 a) b) c) d) T1 A1, B0, R2 T4 A1, B1 A2, B0, R1 A0, B2, R2 T4 T1 T2 T5 T6 A0, B0, R1, R2 A0, B1, R1 T3 T1 A1, B0, R2 T4 A2, B0, R1, CP1 A0, B2, R2, CP1 T2 T5 T6 A0, B0, R1, R2, CP1 A0, B1, R1 T3 T1 A1, B0, R1, R2 T4 A1, B1, R1 A2, B0, R12A0, B2, R1, R2 T4 T1 T2 T5 T6 A0, B0, R12, R2 A0, B1, R12 T3 A1, B2, R2 A2, B2, R1 T5 T1 T2 T6 T6 T1 A1, B0, R1', R2 T4 A1, B1, R1' A2, B0, R1, R1' A0, B2, R1, R2 T4 T1 T2 T5 T6 A0, B0, R1, R1', R2 A0, B1, R1, R1' T3 A1, B2, R2 A2, B2, R1 T5 T1 T2 T6 T6 T3 T3 R2 T5 T6 B1 B2 T1 T2 T3 T4 A0 A1 A2 B0 R1 R2 T5 T6 B1 B2 T1 T2 T3 T4 A0 A1 A2 B0 R1 CP1 R2 T5 T6 B1 B2 T1 T2 T3 T4 A0 A1 A2 B0 R1 Figure 3.9:a) S3PR net which is non-live. b) The net in a) enforced to be live by the addition of the virtual resource CP1 computed from the bad siphon {A2,B2,R1,R2}.c) The net in a) that becomes live by the addition of an extra copy of the type of resource R1. d) The net in a) that becomes live by splitting the resource type R1 into two new resource types, R1 and R1’, and each one is used in a private way by one of the process plans. 118 3. The liveness problem: Characterisation, analysis and synthesis effect produced by each one in the behavior of the corrected net. The net in Fig. 3.9.a is non-live because of the reachable marking [A1 + B1] (a total deadlock) that appears in the reachability graph depicted on the right of the Petri Net. Figure 3.9.b illustrates the result of the application of the liveness enforcing technique presented in Subsection 3.2.2. In effect, in this net there exists the bad siphon {A2,B2,R1,R2}that becomes empty at the marking [A1 + B1]. Therefore, from this siphon and the initial marking of the net the method computes the virtual resource place CP1 depicted in the figure with an initial marking equal to 1. This virtual resource (constraint) produces the removal of the deadlock marking [A1 + B1] as the reachability graph on the right of the figure points out. In other words, CP1 forbids the reachability of the state [A1 + B1]. In this section we propose the increase of the number of copies of some original resource place. A first approach would advocate for increasing in one unit the initial marking of one of the resources involved in the formation of the deadlock. In this case the two resources R1 and R2 are involved in the deadlock because they belong to the unique minimal bad siphon of the net: {A2,B2,R1,R2}. In order to enforce liveness, the resource R1 is selected and one extra token is added to the initial marking, i.e., one extra copy of the resource type R1 is added to the system as it is illustrated in Fig. 3.9.c. The effects on the behavior of the corrected model is that all states of the original net are preserved in the corrected net or at least can be identified. The other effect is that new states appear in the reachability graph allowing to recover the system from the deadlock state to a safe state. The result is that the net becomes live. Nevertheless, the reader can observe that with this technique the bad siphons of the original net persist in the corrected net model, and then from a structural point of view the problem has not been fixed. In effect, if you increase the initial marking of the idle place A0 making it equal to 2 tokens, then the net system becomes non-live. The method proposed in this section is illustrated by means of the net in Fig. 3.9.d. We increase the number of copies of resources, but in order to fix the problem at a structural level this extra copy is of a resource type different to the preexisting copy. In other words, the resource type R1 is split into two different resource types R1 and R1’, each one containing one copy (one copy more than in the original situation with only the resource type R1), and each one of these resource types is used in a private way from only one process plan. The resulting behavior is very similar to the previous one: the original states are maintained and new states appear allowing to recover from the deadlock state to a safe state. Nevertheless, the reader can observe that with this approach the split of R1 has broken the original bad siphon and now there are not bad siphons in the net. This means that if we have an acceptable initial marking in the net, the net will be live. Finally, it is interesting to observe that the techniques based on the addition of copies of resources allow to maintain or even increase the existing concurrency in 3.2. On siphon-based liveness enforcing in FMSs 119 the original net. The other interesting effect is that the method of virtual resources constrain the allocation of resources sequentialising the processes and therefore the resource utilisation ratio is lower than in the case of the additional copies of existing resources. The implementation of this technique requires the analysis of the structure of the net identifying the structural regions (also called zones) in the net wherein a copy of a resource is used in a continuous way. These structural regions are the candidates to use the copies of the resource they need in a private way. In the following section, in order to illustrate the approach we introduce a subclass of S4PR nets named SOAR2 nets that were originally introduced to model minimal adaptive routing algorithms of AGV systems [Rov11]. In this class of nets we define the concept of structural region as an structural object wherein a copy of a type of resource is used in a continuous way, the relations between those objects and the relations of the structural regions with the siphons of the net. The latter allow to identify the structural regions where a privatisation of the use of the copies of some resources would break all the siphons of the net. Taking into account that the method will maintain the corrected net inside the class of the S4PR nets, and the corrected net has an acceptable initial marking, then the net will be live. The class of nets SOAR2and its related properties The SOAR2class of nets is a strict subclass of the S4PR nets. The acronym stands for “S4PR with Ordered Allocation and Release of the Resources”. This class was introduced in the PhD thesis of C. A. Rovetto to model minimal adaptive routing algorithms of objects or data between a source station/node and a destination station/node throughout a system for the guidance of automated vehicles or an interconnection network composed of communication channels. Therefore, the constraints imposed to define the class from the S4PR class come from the application domain and are justified by the application domain. The main properties characterising this subclass with respect to the general class of S4PR are the following: •The order in which the resources (rails or channels) are requested and allocated following a given route, is the same order in which these resources are released. •A process in an intermediate step can have allocated simultaneously a set of resources. •In a change of the state of a process (occurrence of a transition) only one single operation of allocation or release over a unique copy of a type of resource can be executed. In other words, it is not possible to have concurrency between operations of allocation/release of copies of resources. 120 3. The liveness problem: Characterisation, analysis and synthesis •For each type of resource there is only a unique copy of resource belonging to this type of resource. The translation of the previous characteristics to Petri net terms related to the superclass of S4PR gives rise to the following structural constraints and to some constraints for the acceptable initial markings valid for these nets. 1. In each circuit of each state machine of the net, the resources are released in the same order than they were allocated. 2. In each transition of the net, it is only possible to find a unique resource place connected to the transition. If the arc connecting the place inputs in the transition, this represents an allocation operation. If the arc connecting the place outputs from the transition, this represents a release operation. 3. A net of the SOAR2class is an ordinary Petri net, i.e. the weight of all arcs is equal to one. 4. The acceptable initial marking of all resource places in SOAR2nets is equal to 1. In the above constraints on the class of S4PR to obtain the SOAR2class, the three last constraints are more or less easy to understand and to manage. Nevertheless, the first constraint requires the introduction of some new objects named structural regions of continuous use of a copy of resource (shortened: s-regs). Structural regions were originally called zones of continuous use of a copy of resource or simply resource zones [Rov11]. This concept is not only renamed, but generalised, in the context of this PhD thesis. The properties of these structural objects individually considered, and the relations defined over the set of s-regs are the basis of the new deadlock prevention technique intuitively introduced in the previous subsubsection. In the following, these concepts will be introduced with the aid of some examples. An structural region jof continuous use of a copy of the resource rin the i-th process subnet of an SOAR2net is a maximal set of process places that are holders of the resource r,Sr i,j, such that the subnet generated by the s-reg and its input and output transitions is a connected state machine. In the upper process subnet of the SOAR2net of Fig. 3.10 it is possible to find the following set of s-regs: SR1 1,1= {A1,A2,A3},SR2 1,1={A2,A3,A4}and SR3 1,1={A3,A4,A5}. In a similar way, the s-regs of the bottom process subnet are: SR1 2,1={B1,B2},SR2 2,1={B2,B3,B4}and SR3 2,1={B4,B5}. For a resource rwe can find s-regs that belong to different process subnets, and obviously they will be disjoint because they belong to disjoint state machines. It is also possible to find, for a resource r, several s-regs belonging to the same process subnet. Obviously, in this last case the s-regs must be disjoint. Other 3.2. On siphon-based liveness enforcing in FMSs 121 R3 R1 A0 R2 B0 S2,1 R3 S2,1 R2 S2,1 R1 T7 T8 T9 B1 B2 T10 B3 T11 B4 T12 B5 S1,1 R1 S1,1 R2 S1,1 R3 T1 T2 A1 A2 T3 T4 A3 T5 A4 T6 A5 Figure 3.10: A SOAR2net with two process subnets. The set of contained s-regs is depicted in shadowed boxes important property is that the idle place cannot belong to any s-reg because the idle place cannot be a holder place of a resource (recall that the SOAR2class is a strict subclass of the S4PR class of nets). The set of all s-regs of a net will be denoted as ˜ S, and the set of s-regs associated to a resource rwill be denoted as ˜ Sr The first important relation between s-regs is the overlapping relation between s-regs. We say that a set of s-regs A⊆˜ S,A6=∅is a set of overlapping s-regs if and only if TS∈AS6=∅. That is, the set of places belonging to the intersection of a set of s-regs are simultaneously holder places of all resource places associated to the s-regs of the set. In other words, the places of the intersection are process places and a token inside one of these places (a process) is using a copy of each resource associated to the s-regs of the set. Therefore, the computation of the maximal sets of overlapping s-regs is important for the study of the ordering relations in the allocation and release of the set of resources that simultaneously are held by a process inside one of the places in the intersection. For example, for the upper process subnet in Fig. 3.10 there is only one maximal set of s-regs: {SR1 1,1,SR2 1,1,SR3 1,1}. Observe that, SR1 1,1∩SR2 1,1∩SR3 1,1={A3}. In other words, when we have a token inside the place A3, the process is using simultaneously the resources R1, R2 and R3. Observe, that 122 3. The liveness problem: Characterisation, analysis and synthesis Maximal set of Order overlapping s-regs relation {SR1 1,1,SR2 1,1}SR1 1,1<SR2 1,1 {SR2 1,1,SR3 1,1}SR2 1,1<SR3 1,1 {SR1 1,2,SR3 1,1}SR3 1,1<SR1 1,2 {SR1 2,1,SR2 2,1,SR3 2,1}SR3 2,1<SR2 2,1<SR1 2,1 S1,1 R1 S1,1 R2 S1,1 R3 S1,2 R1 S2,1 R3 S2,1 R2 S2,1 R1 R2 R1 R3 T1 T2 T3 A1 A2 T4 A3 T5 T6 A4 A5 T7 A6 T8 A7 A0 T9 T10 B1 T11 B2 T12 T13 B3 B4 T14 B5 B0 Figure 3.11: A SOAR2net, the maximal sets of overlapping s-regs and the order relation between s-regs in order to reach this situation the allocation of these resources happened in the order R1 −R2 −R3. The moving of the token outside the set of overlapping s-regs release the three resources in the same order: the condition imposed for SOAR2 nets. However, in the bottom process subnet in Fig. 3.10 there are two maximal sets of overlapping s-regs: {SR1 2,1,SR2 2,1}and {SR2 2,1,SR3 2,1}. In these two maximal sets the allocation order of the resources is respected in the release process. The order relation in the allocation of resources and its further release, induces an order relation on the set of s-regs that is called pruning relation between s-regs. Taking into account that it is a total order relation in a maximal set of overlapping sregs we are only interested in the maximal chains of ordered elements in the set. This order relation can be represented by means of a graph. In Fig. 3.11 the reader can find a SOAR2net and in the first column of the table the maximal sets of overlapping s-regs. The second column represents the maximal chains of ordered elements in the 3.2. On siphon-based liveness enforcing in FMSs 123 R1 R2 R3 a) b) S1,1 R1 S1,1 R2 S1,1 R3 S1,2 R1 S2,1 R3 S2,1 R2 S2,1 R1 Figure 3.12: Pruning graph of the s-regs of the SOAR2net in Fig. 3.11 and the agglomerated resource pruning graph of the net set. This ordering relations can be represented in a graphical way in the pruning graph of s-regs. Observe that the union of all s-regs associated to a same resource gives as result the set of holders of the resource that together with the resource allow to obtain the support of the minimal p-semiflow associated to the resource. The agglomeration, in the pruning graph of s-regs, of all s-regs of a same resource in a single node allows to obtain the pruning graph of resources used to characterise the siphons [CRC12]. This agglomeration operation in the pruning graph of s-regs is illustrated in Fig. 3.12. The left figure represents the pruning graph of s-regs, wherein the nodes inside the shadowed boxes correspond to the s-regs associated to the same resource and are the nodes to be fused in a single node. Therefore each box gives rise to a node of the right figure in Fig. 3.12. The arcs in the right figure have its origin in the order relation (pruning relation) between two s-regs associated to different resources but overlapped. We must recall that a necessary condition to obtain a siphon containing a given set of resources is that the subgraph of the pruning graph containing the nodes associated to the considered resources and the arcs among them is a strongly connected subgraph. Therefore, if we transform our net in such a way that the resulting pruning graph is acyclic, then we cannot obtain siphons with more than one resource (i.e., the bad siphons of the net causing the non-liveness problems). That is, the acyclic pruning graph obtained after the transformation evidences that the liveness property has been enforced. 124 3. The liveness problem: Characterisation, analysis and synthesis A new deadlock prevention policy based on the specialisation of resources In this section we present a new deadlock prevention technique for the previously introduced class of SOAR2nets. We have presented the advantages of the technique from the point of view of the maintenance (or even increase) of the concurrency of the system and the improvement of the resource utilisation ratio in comparison with other deadlock prevention techniques. Nevertheless, there is another reason for the introduction of this technique: the implementation of the control places added to enforce liveness. In effect, in the methods presented in the previous section, the new control place computed for the liveness enforcing property can be difficult to implement because our new virtual resource is used to control the number of tokens inside a siphon and the arcs of this virtual place can need to be connected to several transitions that are not local. This non-locality of the transitions connected to the new resource place can give rise to new problems with respect to a distributable implementation. The technique we summarise in the following respects this locality principle because the area of intervention in order to enforce the liveness property is constrained to an s-reg and then the implementation issues related to distributability are solved. The basis of the method to correct the model consists of, in the case we have deadlock states, the transformation of the Petri net in such a way that the pruning graph of resources of the transformed net becomes acyclic. Therefore, and according to the characterisation of the minimal siphons of a S4PR net on the pruning graph of resources, there exist no minimal siphons containing more that one resource since there are not strongly connected sub-graphs containing more that one node. This is the basis of the method because in this way we enforce the net to be live since the Petri net has an acceptable initial marking and there are not bad siphons in the net. In order to reach this final goal the designer must follow the steps stated in the following for SOAR2nets: Step 1. Construction of the pruning graph of the s-regs of the net. The net in Fig. 3.13, used as illustrative example in this subsection, is a non-live SOAR2 net. In effect, the graph on the right hand of the figure is the pruning graph of resources that, as the reader can observe, contains one cycle. In this case, the cycle exists because of a bad siphon containing the resource places R1 and R2: the minimal siphon D={R1,R2,A2,A3,B2,B3}. This siphon is emptied by firing the transitions T1 and T5 from the initial marking. In general, the existence of cycles in the resource pruning graph is only a necessary condition for the existence of bad siphons, but if we can make acyclic the graph then it is ensured that no bad siphon exists, and the resulting net is live. To accomplish this, we first must compute all the s-regs, and after that we must compute the maximal set of overlapping s-regs. This lets us construct the pruning graph of 5.4. On detecting bad markings 227 and every clause Cj, with j∈INF, results in a process subnet where ojis the idle place. The resource places of the net are kc and every xi, xi. It is also true that the marking m0is an acceptable initial marking for NF, where: •m0[kc] = Nc, •∀j∈[1,Nc] : m0[oj] = 1, •∀i∈[1, k] : m0[xi] = Nxi,m[xi] = Nxi, •The rest of the places are empty in m0. Moreover, the marking m0is reachable from m, by firing the sequence σ= t1t2... tNc. In Fig. 5.7 it is depicted the resulting net system hNF,mifor the formula F= x2(x1+x2)x2. Obviously, SAT(F) returns NO since the formula is not satisfiable for any possible truth assignment. Theorem 5.16. SAT →S4PR-RIM Proof. Let us prove that SAT(F) returns YES iff S4PR-RIM(NF,m0,m) returns YES. It is obvious that m0∈RS(N,m) iff exists a firing sequence σ,mσ −→m0such that ∀j∈[1,Nc]∃i∈[1,k] such that vj,i, wj,i and zj,i appear in σ. In order to fire some wj,i from a marking m0,m0∈RS(N,m), however, it is required that m0[kc] = Nc. This is, all the tokens in P0∪PSshould be in the places labelled dj0,i0or oj0, for any j0,i0. But for marking any oj0it is again required that some wj0,i0is fired, so the problem can be reduced to: m0∈RS(N,m0) iff exists m∈RS(NF,m0) such that ∀j∈[1,Nc]∃|i∈[1,k] such that m[dj,i] = 1 (thus, m[kc] = Nc,m[aj] = m[bj,i] = m[ej,i] = m[oj] = 0). Now the same reasoning than in the demonstration of Theorem 5.8 can be followed, taking into account that the transitions tj,i are now called uj,i, and we conclude. Returning to the example in Fig. 5.7, it can be verified that m0is not reachable by any means, since there is no reachable marking m0such that m0[kc] = 3, and this implies that the transitions wi,j (according to the notation in Fig. 5.6) are dead, and the idle places ojcannot ever be marked. Finally: Theorem 5.17. S4PR-RIM is NP-complete. Proof. S4PR-RIM is NP-hard since, by Theorem 5.16,SAT is reducible to S4PR-RIM, and it is also NP-easy by Theorem 5.14. 228 5. Some complexity results on the resource allocation problem 3 x1 o2 o1 kc x2 x2 a3 3 3 1 1t a t a2 2 t3 2 2 3 3 3 3 o3 3 Figure 5.7: SAT →S4PR-RIM. Example: F=x2(x1+x2)x2. Summing up, S4PR-DD is co-NP-complete (i.e., optimal deadlock detection in the S4PR is co-NP-complete)2. The problem of deciding if the firing of a transition is safe for applying optimal deadlock avoidance techniques remains NP-complete for the S4PR class. 5.5 On detecting spurious markings A spurious marking is a solution of the net state equation, m=m0+C·x,x0, that is not reachable from m0. A killing spurious solution is a spurious marking such that hN,miis non-live. There exist Petri net subclasses, such as EQ systems [TS93], for which killing spurious solutions are not possible. In those cases, the linear description 2However, we remind the reader that there exists a reachable marking m0such that it can be structurally characterised as a bad marking by Theorem 1.4, but this does not affect the inherent computational complexity of the problem. 5.6. Conclusions 229 provided by the net state equation can be used to determine the liveness of the system. Unfortunately, the S4PR class is not one of those classes, and this limits the potential of the net state equation for this purpose. Unless that, noticeably, spurious solutions were efficiently detectable for a given S4PR system. As will be seen, however, this is a co-NP-complete problem: Problem 5.18. S4PR-Spurious-Detection (S4PR-SD) Given: An S4PR net system hN,m0i, being m0an acceptable initial marking, and m∈IN|P|,m=m0+C·x,x≥0. To decide: Is man spurious marking? Intuitively, mis an spurious marking iff m0is not reachable from min its reverse (note that there may be isolated spurious solutions, i.e. not connected to the reachability space). Meanwhile, the reverse net of an S4PR net is another S4PR net. This is quite trivial, since the polarity inversion of the incidence matrix does not affect its (left or right) annullers, so the p and t-semiflows are preserved with respect to N. It is easy to see now that S4PR-SD is co-NP-complete. This is bad news since, unless NP=P, this implies that it cannot be verified that a marking is spurious in deterministic polynomial time using solely the structure of the net. 5.6 Conclusions RASs are abstractions of real systems allowing to concentrate on the study of problems such as deadlocks due to the sharing of resources used in mutual exclusion. Modelling RASs with Petri nets is particularly easy through the identification of processes with state machines and resources with monitor places representing the allocation of copies of resources. As a consequence, the S4PR subclass has already been proven specially useful and suitable for the RAS abstraction of FMSs [TGVCE05], but can be applied in many other different contexts. To illustrate this fact, a motivating example was introduced in order to depict the utility of the conceptual framework in the study and correction of deadlock problems in distributed systems and protocols, beyond the FMS context. More importantly in the context of this thesis, S4PR nets can be rather handy as a restricted, powerful model for tackling certain simple multithreaded software systems. Nevertheless, this is a most general class of models for which structural results exist characterising non-liveness. For this reason, it has been addressed an insight on the complexity of some problems related to handling with deadlocks using this kind of models. As expected, many of the important problems are proven computationally intractable, and for this reason, the heuristics presented by F. Tricas et al. [Tri03, 230 5. Some complexity results on the resource allocation problem TGVCE05] have special interest. Obviously these results also work as lower bounds of computational complexity for the (more general) class of PC2Rnets. Regarding optimal deadlock prevention, it has been established that the problem of determining if an S4PR net system is non-live is NP-complete. Besides, evidence has been provided for NP-completeness of optimal deadlock avoidance for this class, generalising earlier results for other types of RASs which were already proven NP-hard. This was accomplished thanks to proving the equivalence of this problem with that of deciding the reachability of the initial marking. The inverse problem (optimal deadlock detection, in the strictest sense) is co-NP-complete. Moreover, because the mathematical methods presented by Tricas et al. [TGVCE05] are based on the net state equation, an insight on the complexity of the detection of spurious markings is also relevant. The intractability of the problem, along with the existence of killing spurious solutions, constrains the practicality of the net state equation for determining non-liveness. Conclusions During recent times, Petri nets have emerged as a powerful modeling paradigm for dealing with the problem of allocation of shared resources in concurrent systems. So attests the gradual flourish of Petri net-based analysis and synthesis techniques based on the study of structural properties in RASs composed of sequential processes and shared resources. Such approaches are framed within a methodological context which advocates for a first study and correction of the problems caused by resource sharing, prior to addressing other systemic problems. The application of structural correction techniques allows that the outcome of this process can survive subsequent system refinements. In essence, this approach is based on the principle that the so-named RAS view of a system is but one of many facets of the system, which is observed through a prior process of abstraction that allows applying this type of techniques on concurrent systems belonging to enormously varied application domains. This PhD thesis attempts to bring such techniques to the context of multithreaded programming, which due to its inherent complexity presents serious difficulties when it comes to successfully adapt the classical results in the field, and particularly to obtain live multithreaded software systems. First, Chap. 1has presented a comprehensive overview on the RASs from an essentially systemic point of view. In that sense, the chapter attempts to shed light on some aspects rarely present in the literature. First, it identifies the basic principles of the proposed methodology and puts in value the abstraction process leading to obtaining a view of the system based on processes and resources that is easily translatable to Petri net models. In that sense, the process of abstraction has been structured, identifying some of the usual features that allow categorising processes and resources at the time of their identification. Discursively, that has been integrated with the presentation of the RAS abstraction of different application domains from the literature, projecting the features identified on these domains. As a result of this process, it has been observed that there are often abundant commonalities because of which the resulting Petri net models often belong to a restricted family of subclasses. These subclasses have been introduced, compared and classified with respect to their modeling capabilities. As a paradigm of these subclasses, S4PR has been presented as 231 232 Concluding Remarks the one representing the final frontier, since it is the most general subclass for which there exist structural results characterising liveness, which facilitates the application of synthesis techniques for liveness enforcing. Next, an RAS view of multithreaded software systems is discussed in Chapter 2. As a result, we have presented a list of requirements that an RAS model must meet to be able to model with sufficient versatility the richness of such systems. In parallel, it has also been detected that those earlier models exploited in the literature are not sufficient to meet that objective. Consequently, we have presented a new class of Petri nets, called PC2R, which generalises the previous RAS subclasses and fully meets the above requirements. Unfortunately, after crossing the Rubicon it has been observed that finding some sort of structural liveness characterisation is a complicated task in general for such complex systems. Some of the behavioural and structural properties of these nets have been explored and compared to those found in more restricted subclasses, therefore reaching a twofold objective. First, a general overview of the family of classes to model RASs has been sketched; not only from a syntactical point of view (the classical approach in this type of work) but also from a behavioural one. And second, we have remarked some major obstacles encountered when approaching into more complex systems such as multithreaded software systems to address the problem of enforcing liveness. In addition, certain instruments are defined, such as the shrinking graph, which are useful for addressing subsequent analysis and synthesis techniques along Chap. 3that allow dealing with the anomalous situations. In Chap. 3, a review and categorisation of those Petri net-based techniques for enforcing liveness in the literature has been addressed. In particular, it has been proved that the classical control theory based on the restriction of firing sequences to inhibit abnormal behaviour by adding virtual resources which act as monitors is in general difficult to apply in multithreaded software systems. Rather, in this context such techniques are relegated to subclasses of systems (or subsystems of them) in which resources are used under certain significant restrictions. However, new techniques based on the addition of behaviour through the privatisation of resources, originally raised in the context of the construction of minimum adaptive deadlock-free routing algorithms for interconnection networks [Rov11], are revealed as a promising direction for obtaining live systems from a different approach. The above results have been approached from the application domain under study in this thesis. The result is a toolbox of heuristics to transform and correct, in a modular manner, multithreaded software systems modelled through the PC2Rclass. This required to investigate the peculiar characteristics and complex properties that siphons present in nets of such kind, as well as to define or refocus the constructive elements that allow deploying this type of techniques. In addition, a bridge has been established with classical structural theory, introducing sufficient or necessary conditions that collapse in the characterisation for simpler subclasses, thus outlining the disruption frontier of the Concluding Remarks 233 classical results. Gadara [WLR+09] is a subclass of Petri nets introduced to deal with the deadlock problem due to the emergence of circular waits on binary mutexes in multithreaded software. Although the structure of each process of a Gadara net is modelled by means of a (general) state machine, this type of model presents a number of restrictions with respect to the PC2Rclass (e.g., binary mutexes, resources that do not participate in the internal choices, etc.) that constrain their application to a limited subclass of multithreaded software systems. In Chap. 4bridges have been established with the family of RAS models in the literature. In particular it has been shown that Gadara nets are strongly related to a subclass of S4PR in which the internal allocation of resources to a process is deterministic. In addition, tools are provided to move from one to the other net subclass, and a formal, exhaustive proof has been presented for a siphon-based liveness characterisation for a superclass of Gadara nets: a result that, despite already being stated for Gadara nets [WLR+09], remained publicly unproven at the time of publishing our work [LGC11]. Finally, given the existing relations between the different subclasses of RASs and the special place occupied by S4PR among all these subclasses, Chap. 5introduces a formal study of the computational complexity inherent to various problems related to the application of liveness enforcing techniques in systems modelled through the S4PR subclass. This subclass of nets is capable of modelling the RAS abstraction of some simple multithreaded software systems. In particular, it has been proved that most of the interesting problems of such systems regarding liveness fall within the family of NP-complete or co-NP-complete problems. This intractability formally justifies the search for efficient heuristics that imbues the literature and the pragmatical approach pursued in some of the results presented in previous chapters. Furthermore, these results mark a lower bound of computational complexity to more complex systems such as those addressed in the context of the first chapters: the PC2Rclass, for instance. 234 Concluding Remarks Appendix A Basic Petri nets notation APlace/Transition (P/T) is a 4-tuple N=hP, T, F, W i, where F⊆(P×T)∪(T× P) is the set of arcs, and Wis a total function W:F→IN+, being P,Tnon empty, finite and disjoint sets. Elements belonging to the sets Pand Tare called respectively places and transitions, or generally nodes. P/T nets can be represented as a directed bipartite graph, where places (transitions) are graphically denoted by circles (rectangles): let p∈P,t∈T,u=W(p, t), v=W(t, p), there is a directed arc, labelled u(v), beginning in p(t) and ending in t(p) iff (p, t)∈F((t, p)∈F). The preset (poset) or set of input (output) nodes of a node x∈P∪Tis denoted by •x(x•), where •x={y∈P∪T|(y, x)∈F}(x•={y∈P∪T|(x, y)∈F}). The preset (poset) of a set of nodes X⊆P∪Tis denoted by •X(X•), where •X={y|y∈•x, x ∈X}(X•={y|y∈x•, x ∈X} An ordinary P/T net is a net with unitary arc weights (i.e., ∀(x, y)∈F:W(x, y) = 1, and hence Ncan be defined with a 3-tuple hP, T, F i). If the arc weights can be non-unitary, the P/T net is also called generalised. A state machine is an ordinary net such that for every t∈T,|•t|=|t•|= 1. An acyclic state machine is an ordinary net such that for every t∈T,|•t| ≤ 1, |t•| ≤ 1, and there is no circuit in it. A self-loop place p∈Pis a place such that p∈p••. A pure P/T net (also self-loop free P/T net) is a net with no self-loop places. In pure P/T nets, the net can be also defined by the 3-tuple N=hP, T, Ci, where Cis called the incidence matrix, and C=Post −Pre, with Pre[p, t] = W(p, t) iff (p, t)∈F(otherwise, Pre[p, t] = 0) and Post[p, t] = W(t, p) iff (t, p)∈F(otherwise, Post[t, p] = 0). Nets with self-loop places can be easily transformed into pure P/T nets without altering most significant behavioural properties, such as liveness, as shown in Fig.A.1. Ap-flow (t-flow) is a vector y∈ZZ|P|,y6=0(x∈ZZ|T|,x6=0), which is a left (right) annuler of the incidence matrix, y·C=0(C·x=0). The support of a p-flow (t-flow), denoted kyk(kxk), is the set of places (transitions) for which 235 236 A. Basic Petri nets notation T’’ nn PP mm T T’ Figure A.1: Transformation rule: Removing self-loop places their corresponding components in the p-flow (t-flow) are not zero, i.e., kyk={p∈ P|y[p]6= 0}(kxk={t∈T|x[t]6= 0}). The aforementioned places (transitions) are said to be covered by y(x). A minimal p-flow (minimal t-flow) is a p-flow (t-flow) such that the g.c.d of its non-null components is one and its support kyk(kxk) is not an strict superset of the support of another p-flow (t-flow). A p-semiflow (t-semiflow) is a non-negative p-flow. The P/T net Nis conservative (consistent) iff every place (transition) is covered by a p-semiflow (t-semiflow). A set of places D⊆P(Θ ⊆P) is a siphon (trap) iff every place p∈•D(p∈Θ•) satisfies p∈D•(p∈•Θ). The support of a p-semiflow is a siphon (trap) but the opposite does not hold in general. Let N=hP, T, F, Wibe a P/T net, and let P0⊆Pand T0⊆T, where P0, T06=∅. The P/T net N0=hP0, T0, F 0, W0iis the subnet generated by P0,T0iff (x, y)∈ F0⇐⇒ (x, y)∈Fand W0(x, y) = W(x, y), for every pair of nodes x, y ∈P0∪T0. Let N=hP, T, Cibe a pure P/T net. Its reverse net Nr=hP, T, Criis the same net with its arcs inverted, i.e. ∀p∈P, t ∈T:Cr(p, t) = −C(p, t). Its dual net Nd=hPd, Td,Cdiis the result of replacing every place of Nwith a transition, and viceversa, i.e. Pd=T,Td=Pand ∀p∈Pd, t ∈Td:Cd(p, t) = C(t, p). Amarking mof a P/T net Nis a vector of IN|P|, assigning a finite number of tokens m[p] to every place p∈P. Tokens are usually represented by black dots within the places. The support of a marking, kmk, is the set of places which are marked in m, i.e. kmk={p∈P|m[p]6= 0}. We define a marked P/T net (also P/T net system) as the pair hN,m0i, where Nis a P/T net, and m0is a marking for N, also called initial marking.Nis said to be the structure of the system, while m0 represents the initial state of the system. Throughout this thesis, net markings are usually denoted in the form: [PK1 1,PK2 2, ..., PKn n], with K1, ..., Kn∈IN. For a marking mdenoted in this way, the naturals K1, ..., Knrepresent the values of the vector m corresponding to the places P1, ..., Pnof the net, i.e., ∀i∈[1, n] : m[Pi] = Ki. The rest of components of the vector mare assumed to be zero-valued. Also in the context of this PhD thesis, p-semiflows are often represented as marking invariants in the form: K1·m[P1] + K2·m[P2] + (...) + Kn·m[Pn] = K0, with K1, 243 (T2,A1);(T4,A3) R2 R1 R3 (T3,A2) (T5,A2) (T8,B1) Figure B.6: Resource pruning graph of the net in Fig. 3.22 (T2,A1);(T4,B0) R2 R1 R3 (T6,B2) (T1,A0);(T6,B2); (T8,C1) (T7,C0) (T2,A1);(T4,B0) (T1,A0);(T5,B1);(T8,C1) Figure B.7: Resource pruning graph of the net in Fig. 3.23 244 B. Some additional examples and figures (T2,A1);(T5,A4); (T8,B0);(T11,B3) R2 R1 R4 R3 R5 (T3,A2); (T6,A5); (T9,B1); (T12,B4) (T7,A6); (T10,B2) (T7,A6) (T13,B5) (T14,B6) (T6,A5) (T5,A4) (T1,A0) (T4,A3); (T10,B2) (T4,A3); (T13,B5) (T11,B3) (T12,B4) Figure B.8: Resource pruning graph of the net in Fig. 3.24 245 A1, R1, R2 A2, R3 T2 A3, R1, R3 T3 A4, R2, R3 A0 T6 T1 T5 T4 Figure B.9: Reachability graph of the net in Fig. 3.26 (T6,A4) R2 R1 R3 (T4,A3) (T2,A1) (T4,A3) (T6,A4) (T2,A1) Figure B.10: Resource pruning graph of the net in Fig. 3.26 246 B. Some additional examples and figures Bibliography [BV84] E. Best and K. Voss. Free choice systems have home states. Acta Informatica 21, pages 89–100, 1984. [BZB+97] R. Brade, L. Zhang, S. Berson, S. Herzog, and S. Jamin. RFC 2205: Resource ReSerVation Protocol – Version 1 Functional Specification, September 1997. [CES71] E.G. Coffman, M. Elphick, and A. Shoshani. System deadlocks. ACM Computing Surveys, 3(2):67–78, 1971. [Col03] J-M. Colom. The resource allocation problem in flexible manufacturing systems. In W.M.P. van der Aalst and E. Best, editors, Proc. of the 24th Int. Conf. on Applications and Theory of Petri Nets, volume 2679 of LNCS, pages 23–35, Eindhoven, Netherlands, June 2003. SpringerVerlag. [Col11] Collins English Dictionary. HarperCollins Publishers, 2011. [CRC12] E.E. Cano, C.A. Rovetto, and J-M. Colom. An algorithm to compute the minimal siphons in S4PR nets. Discrete Event Dynamic Systems, 22(4):403–428, 2012. [CS91] J-M. Colom and M. Silva. Improving the linearly based characterization of P/T nets. In Rozenberg, G., editor, Advances in Petri Nets 1990, volume 483 of LNCS, pages 113–145. Springer-Verlag, Berlin, Germany, 1991. [CX97] F. Chu and X.L. Xie. Deadlock analysis of Petri nets using siphons and mathematical programming. IEEE Transactions on Robotics and Automation, 13(6):793–804, December 1997. [Dij67] E.W. Dijkstra. The structure of the “THE”-multiprogramming system. In Proc. of the 1st ACM Symposium on Operating System Principles, SOSP ’67, pages 10.1–10.6, New York, NY, USA, 1967. ACM. 247 248 Bibliography [Dij82] E.W. Dijkstra. The mathematics behind the Banker’s Algorithm. Selecting Writings on Computing: A Personal Perspective, pages 308–312, 1982. [DS86] W.J. Dally and L. Seitz. The torus routing chip. Distributed Computing, 1(4):187–196, 1986. [Dua95] J. Duato. Necessary and sufficient condition for deadlock-free adaptive routing in wormhole networks. IEEE Transactions on Parallel and Distributed Systems, 6(10):1055–1067, 1995. [ECM95] J. Ezpeleta, J-M. Colom, and J. Mart´ınez. A Petri net based deadlock prevention policy for flexible manufacturing systems. IEEE Transactions on Robotics and Automation, 11(2):173–184, April 1995. [EGVC98] J. Ezpeleta, F. Garc´ıa-Vall´es, and J-M. Colom. A class of well structured Petri nets for flexible manufacturing systems. In J. Desel and M. Silva, editors, Proc. of the 19th Int. Conf. on Application and Theory of Petri Nets, volume 1420 of LNCS, pages 64–83, Lisbon, Portugal, June 1998. Springer-Verlag. [ER04] J. Ezpeleta and L. Recalde. A deadlock avoidance approach for nonsequential resource allocation systems. IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans, 34(1):93–101, January 2004. [ETGVC02] J. Ezpeleta, F. Tricas, F. Garc´ıa-Vall´es, and J-M. Colom. A banker’s solution for deadlock avoidance in FMS with flexible routing and multiresource states. IEEE Transactions on Robotics and Automation, 18(4):621–625, August 2002. [Fan02] M.P. Fanti. A deadlock avoidance strategy for AGV systems modelled by coloured Petri nets. In Proc. of the 6th Int. Workshop on Discrete Event Systems (WODES’02), pages 61–66, Washington, DC, USA, 2002. IEEE Computer Society. [FGS06] M.P. Fanti, A. Giua, and C. Seatzu. Monitor design for colored Petri nets: An application to deadlock prevention in railway networks. Control Engineering Practice, 14(10):1231–12472, October 2006. [FMMT97] M.P. Fanti, B. Maione, S. Mascolo, and B. Turchiano. Event-based feedback control for deadlock avoidance in flexible production systems. IEEE Transactions on Robotics and Automation, 13(3):347–363, 1997. Bibliography 249 [FZ04] M.P. Fanti and M.C. Zhou. Deadlock control methods in automated manufacturing systems. IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans, 34(1):5–22, January 2004. [GDS92] A. Giua, F. DiCesare, and M. Silva. Generalized mutual exclusion contraints on nets with uncontrollable transitions. In IEEE International Conference on Systems, Man and Cybernetics, volume 2, pages 974–979, Chicago, USA, October 1992. [GJ79] M.R. Garey and D.S. Johnson. Computers and Intractability: A Guide to the Theory of NP-Completeness. W. H. Freeman & Co., New York, NY, USA, 1979. [Gol78] E. M. Gold. Deadlock prediction: Easy and difficult cases. SIAM Journal on Computing, 7(3):320–336, 1978. [GRX03] A. Ghaffari, N. Rezg, and X.L. Xie. Design of a live and maximally permissive Petri net controller using the theory of regions. IEEE Transactions on Robotics, 19(1):137–142, 2003. [GV99] F. Garc´ıa-Vall´es. Contributions to the structural and symbolic analysis of place/transition nets with applications to flexible manufacturing systems and asynchronous circuits. PhD thesis, University of Zaragoza, Zaragoza, April 1999. [GVC99] F. Garc´ıa-Vall´es and J-M. Colom. Implicit places in net systems. In P. Bucholz and M. Silva, editors, IEEE 8th International Workshop on Petri Nets and Performance Models (PNPM’99), pages 104–113, Zaragoza, Spain, September 1999. IEEE Computer Society Press. [GVTCE98] F. Garc´ıa-Vall´es, F. Tricas, J-M. Colom, and J. Ezpeleta. Optimal control of discrete event systems. In Proc. of the 4th Int. Workshop on Discrete Event Systems (WODES98), pages 88–93, Cagliari, Italy, August 1998. Institution of Electrical Engineers, London. [GW92] F. Giunchiglia and T. Walsh. A theory of abstraction. Artificial Intelligence, 57:323–389, October 1992. [Har80] D. Harel. On folk theorems. Communications of the ACM, 23(7):379– 389, 1980. [Hel13] A. Hellemans. Ring around the nanowire. IEEE Spectrum, 50(5):14–15, May 2013. 250 Bibliography [Hil85] D. Hillen. Relationship between deadlock-freeness and liveness in freechoice nets. Newsletter, (19):28–32, February 1985. [HJXC06] Y.S. Huang, M.D. Jeng, X.L. Xie, and D.H. Chung. Siphon-based deadlock prevention policy for flexible manufacturing systems. IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans, 36(6):1248–1256, 2006. [Hoa78] C. A. R. Hoare. Communicating sequential processes. Communications of the ACM, 21(8):666–677, 1978. [HZL09] H.S. Hu, M.C. Zhou, and Z.W. Li. Liveness enforcing supervision of video streaming systems using non-sequential Petri nets. IEEE Transactions on Multimedia, 11(8):1446–1456, December 2009. [HZL11] H.S. Hu, M.C. Zhou, and Z.W. Li. Supervisor optimization for deadlock resolution in automated manufacturing systems with Petri nets. IEEE Transactions on Automation Science and Engineering, 8(4):794–804, October 2011. [IA06] M.V. Iordache and P.J. Antsaklis. Supervisory Control of Concurrent Systems: A Petri Net Structural Approach. Systems & Control: Foundations & Applications. Birkh¨auser, 2006. [IA07] M.V. Iordache and P.J. Antsaklis. Petri net supervisors for disjunctive constraints. In Proc. of the 2007 American Control Conference, pages 4951–4956, New York, USA, July 2007. [IA09] M.V. Iordache and P.J. Antsaklis. Petri nets and programming: A survey. In Proc. of the 2009 American Control Conference, pages 4994–4999, St. Louis, Missouri, USA, June 2009. [Joh75] D.B. Johnson. Finding all the elementary circuits of a directed graph. SIAM Journal on Computing, 4(1):77–84, 1975. [JX01] M.D. Jeng and X.L. Xie. Modeling and analysis of semiconductor manufacturing systems with degraded behavior using Petri nets and siphons. IEEE Transactions on Robotics and Automation, 17(5):576–588, 2001. [JXC04] M.D. Jeng, X.L. Xie, and S.L. Chung. ERCN* merged nets for modeling degraded behavior and parallel processes in semiconductor manufacturing systems. IEEE Transactions on Systems, Man, and Cybernetics, Part A: Systems and Humans, 34(1):102–112, 2004. Bibliography 251 [JXP02] M.D. Jeng, X.L. Xie, and M.Y. Peng. Process nets with resources for manufacturing modeling and their analysis. IEEE Transactions on Robotics, 18(6):875–889, 2002. [KA99] X.D. Koutsoukos and P.J. Antsaklis. Computational issues in intelligent control: Discrete-event and hybrid systems. In N.K. Sinha and M.M. Gupta, editors, Soft Computing and Intelligent Systems: Theory and Practice, chapter 3, pages 39–69. Academic Press, October 1999. [Kid98] P.A. Kidwell. Stalking the elusive computer bug. IEEE Annals of the History of Computing, 20(4):5–9, October 1998. [KS89] J.F. Kurose and R. Simha. A microeconomic approach to optimal resource allocation in distributed computer systems. IEEE Transactions on Computers, 38(5):705–717, 1989. [Lau02] K. Lautenbach. Reproducibility of the empty marking. In J. Esparza and C. Lakos, editors, Proc. of the 23rd Int. Conf. on Applications and Theory of Petri Nets, volume 2360 of LNCS, pages 237–253, London, UK, 2002. Springer-Verlag. [LDZ06] Z.W. Li, W. Ding, and R.M. Zhu. On deadlock prevention in case of failures in flexible manufacturing systems. International Journal of Manufacturing Technology and Management, 8(1-2):58–74, 2006. [LGC06] J-P. L´opez-Grao and J-M. Colom. Lender processes competing for shared resources: Beyond the S4PR paradigm. In Proc. of the 2006 Int. Conf. on Systems, Man and Cybernetics, pages 3052–3059, Taipei, Taiwan, October 2006. IEEE. [LGC11] J-P. L´opez-Grao and J-M. Colom. On the deadlock analysis of multithreaded control software. In Proceedings of the 16th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA’2011), Toulouse, France, September 2011. [LGC12] J-P. L´opez-Grao and J-M. Colom. A Petri net perspective on the Resource Allocation Problem in software engineering. In K. Jensen, S. Donatelli, and J. Kleijn, editors, Transactions On Petri Nets and Other models of Concurrency V (ToPNoC V), volume 6900 of LNCS, pages 181–200. Springer, Heidelberg, Germany, 2012. [LGCT14] J-P. L´opez-Grao, J-M. Colom, and F. Tricas. Structural deadlock prevention policies for Flexible Manufacturing Systems: A Petri net outlook. In J. Campos, C. Seatzu, and X.L. Xie, editors, Formal Methods in 252 Bibliography Manufacturing, Series on Industrial Information Technology, chapter 7. CRC Press/Taylor and Francis, Toulouse, France, To appear. 2014. [LR01] M.A. Lawley and S.A. Reveliotis. Deadlock avoidance for sequential Resource Allocation Systems: Hard and easy cases. Int. Journal of Flexible Manufacturing Systems, 13:385–404, 2001. [LSW+11] H. Liao, J. Stanley, Y. Wang, S. Lafortune, S.A. Reveliotis, and S. Mahlke. Deadlock-avoidance control of multithreaded software: An efficient siphon-based algorithm for Gadara Petri nets. In Proc. of the 50th IEEE Conf. on Decision and Control and European Control Conference (CDC-ECC 2011), 2011 50th IEEE Conference on, pages 1142–1148. IEEE, December 2011. [LT79] K. Lautenbach and P.S. Thiagarajan. Analysis of a resource allocation problem using Petri nets. In Syre, J.C., editor, Proc. of the 1st European Conf. on Parallel and Distributed Processing, pages 260–266, Toulouse, 1979. Cepadues Editions. [LT93] N.G. Leveson and C.S. Turner. An investigation of the Therac – 25 accidents. IEEE Computer, 26(7):18–41, July 1993. [LWC+13] H. Liao, Y. Wang, H.K. Cho, J. Stanley, T. Kelly, S. Lafortune, S. Mahlke, and S.A. Reveliotis. Concurrency bugs in multithreaded software: Modeling and analysis using Petri nets. Discrete Event Dynamic Systems, pages 1–39, 2013. [LZ08] Z.W. Li and M.C. Zhou. Control of elementary and dependent siphons in Petri nets and their application. IEEE Transactions on Systems, Man and Cybernetics, Part A: Systems and Humans, 38(1):133–148, January 2008. [LZ09] Z.W. Li and M.C. Zhou. Deadlock Resolution in Automated Manufacturing Systems: A Novel Petri Net Approach. Springer, New York, USA, 2009. [Min82] T. Minoura. Deadlock avoidance revisited. Journal of the ACM, 29(4):1023–1048, Oct 1982. [Mur89] T. Murata. Petri nets: Properties, analysis and applications. Proceedings of the IEEE, 77(4):541–580, 1989.