8 resultados para timing constraint
em AMS Tesi di Dottorato - Alm@DL - Università di Bologna
Resumo:
This thesis intends to investigate two aspects of Constraint Handling Rules (CHR). It proposes a compositional semantics and a technique for program transformation. CHR is a concurrent committed-choice constraint logic programming language consisting of guarded rules, which transform multi-sets of atomic formulas (constraints) into simpler ones until exhaustion [Frü06] and it belongs to the declarative languages family. It was initially designed for writing constraint solvers but it has recently also proven to be a general purpose language, being as it is Turing equivalent [SSD05a]. Compositionality is the first CHR aspect to be considered. A trace based compositional semantics for CHR was previously defined in [DGM05]. The reference operational semantics for such a compositional model was the original operational semantics for CHR which, due to the propagation rule, admits trivial non-termination. In this thesis we extend the work of [DGM05] by introducing a more refined trace based compositional semantics which also includes the history. The use of history is a well-known technique in CHR which permits us to trace the application of propagation rules and consequently it permits trivial non-termination avoidance [Abd97, DSGdlBH04]. Naturally, the reference operational semantics, of our new compositional one, uses history to avoid trivial non-termination too. Program transformation is the second CHR aspect to be considered, with particular regard to the unfolding technique. Said technique is an appealing approach which allows us to optimize a given program and in more detail to improve run-time efficiency or spaceconsumption. Essentially it consists of a sequence of syntactic program manipulations which preserve a kind of semantic equivalence called qualified answer [Frü98], between the original program and the transformed ones. The unfolding technique is one of the basic operations which is used by most program transformation systems. It consists in the replacement of a procedure-call by its definition. In CHR every conjunction of constraints can be considered as a procedure-call, every CHR rule can be considered as a procedure and the body of said rule represents the definition of the call. While there is a large body of literature on transformation and unfolding of sequential programs, very few papers have addressed this issue for concurrent languages. We define an unfolding rule, show its correctness and discuss some conditions in which it can be used to delete an unfolded rule while preserving the meaning of the original program. Finally, confluence and termination maintenance between the original and transformed programs are shown. This thesis is organized in the following manner. Chapter 1 gives some general notion about CHR. Section 1.1 outlines the history of programming languages with particular attention to CHR and related languages. Then, Section 1.2 introduces CHR using examples. Section 1.3 gives some preliminaries which will be used during the thesis. Subsequentely, Section 1.4 introduces the syntax and the operational and declarative semantics for the first CHR language proposed. Finally, the methodologies to solve the problem of trivial non-termination related to propagation rules are discussed in Section 1.5. Chapter 2 introduces a compositional semantics for CHR where the propagation rules are considered. In particular, Section 2.1 contains the definition of the semantics. Hence, Section 2.2 presents the compositionality results. Afterwards Section 2.3 expounds upon the correctness results. Chapter 3 presents a particular program transformation known as unfolding. This transformation needs a particular syntax called annotated which is introduced in Section 3.1 and its related modified operational semantics !0t is presented in Section 3.2. Subsequently, Section 3.3 defines the unfolding rule and prove its correctness. Then, in Section 3.4 the problems related to the replacement of a rule by its unfolded version are discussed and this in turn gives a correctness condition which holds for a specific class of rules. Section 3.5 proves that confluence and termination are preserved by the program modifications introduced. Finally, Chapter 4 concludes by discussing related works and directions for future work.
Resumo:
Curved mountain belts have always fascinated geologists and geophysicists because of their peculiar structural setting and geodynamic mechanisms of formation. The need of studying orogenic bends arises from the numerous questions to which geologists and geophysicists have tried to answer to during the last two decades, such as: what are the mechanisms governing orogenic bends formation? Why do they form? Do they develop in particular geological conditions? And if so, what are the most favorable conditions? What are their relationships with the deformational history of the belt? Why is the shape of arcuate orogens in many parts of the Earth so different? What are the factors controlling the shape of orogenic bends? Paleomagnetism demonstrated to be one of the most effective techniques in order to document the deformation of a curved belt through the determination of vertical axis rotations. In fact, the pattern of rotations within a curved belt can reveal the occurrence of a bending, and its timing. Nevertheless, paleomagnetic data alone are not sufficient to constrain the tectonic evolution of a curved belt. Usually, structural analysis integrates paleomagnetic data, in defining the kinematics of a belt through kinematic indicators on brittle fault planes (i.e., slickensides, mineral fibers growth, SC-structures). My research program has been focused on the study of curved mountain belts through paleomagnetism, in order to define their kinematics, timing, and mechanisms of formation. Structural analysis, performed only in some regions, supported and integrated paleomagnetic data. In particular, three arcuate orogenic systems have been investigated: the Western Alpine Arc (NW Italy), the Bolivian Orocline (Central Andes, NW Argentina), and the Patagonian Orocline (Tierra del Fuego, southern Argentina). The bending of the Western Alpine Arc has been investigated so far using different approaches, though few based on reliable paleomagnetic data. Results from our paleomagnetic study carried out in the Tertiary Piedmont Basin, located on top of Alpine nappes, indicate that the Western Alpine Arc is a primary bend that has been subsequently tightened by further ~50° during Aquitanian-Serravallian times (23-12 Ma). This mid-Miocene oroclinal bending, superimposing onto a pre-existing Eocene nonrotational arc, is the result of a composite geodynamic mechanism, where slab rollback, mantle flows, and rotating thrust emplacement are intimately linked. Relying on our paleomagnetic and structural evidence, the Bolivian Orocline can be considered as a progressive bend, whose formation has been driven by the along-strike gradient of crustal shortening. The documented clockwise rotations up to 45° are compatible with a secondary-bending type mechanism occurring after Eocene-Oligocene times (30-40 Ma), and their nature is probably related to the widespread shearing taking place between zones of differential shortening. Since ~15 Ma ago, the activity of N-S left-lateral strike-slip faults in the Eastern Cordillera at the border with the Altiplano-Puna plateau induced up to ~40° counterclockwise rotations along the fault zone, locally annulling the regional clockwise rotation. We proposed that mid-Miocene strike-slip activity developed in response of a compressive stress (related to body forces) at the plateau margins, caused by the progressive lateral (southward) growth of the Altiplano-Puna plateau, laterally spreading from the overthickened crustal region of the salient apex. The growth of plateaux by lateral spreading seems to be a mechanism common to other major plateaux in the Earth (i.e., Tibetan plateau). Results from the Patagonian Orocline represent the first reliable constraint to the timing of bending in the southern tip of South America. They indicate that the Patagonian Orocline did not undergo any significant rotation since early Eocene times (~50 Ma), implying that it may be considered either a primary bend, or an orocline formed during the late Cretaceous-early Eocene deformation phase. This result has important implications on the opening of the Drake Passage at ~32 Ma, since it is definitely not related to the formation of the Patagonian orocline, but the sole consequence of the Scotia plate spreading. Finally, relying on the results and implications from the study of the Western Alpine Arc, the Bolivian Orocline, and the Patagonian Orocline, general conclusions on curved mountain belt formation have been inferred.
Resumo:
This work presents hybrid Constraint Programming (CP) and metaheuristic methods for the solution of Large Scale Optimization Problems; it aims at integrating concepts and mechanisms from the metaheuristic methods to a CP-based tree search environment in order to exploit the advantages of both approaches. The modeling and solution of large scale combinatorial optimization problem is a topic which has arisen the interest of many researcherers in the Operations Research field; combinatorial optimization problems are widely spread in everyday life and the need of solving difficult problems is more and more urgent. Metaheuristic techniques have been developed in the last decades to effectively handle the approximate solution of combinatorial optimization problems; we will examine metaheuristics in detail, focusing on the common aspects of different techniques. Each metaheuristic approach possesses its own peculiarities in designing and guiding the solution process; our work aims at recognizing components which can be extracted from metaheuristic methods and re-used in different contexts. In particular we focus on the possibility of porting metaheuristic elements to constraint programming based environments, as constraint programming is able to deal with feasibility issues of optimization problems in a very effective manner. Moreover, CP offers a general paradigm which allows to easily model any type of problem and solve it with a problem-independent framework, differently from local search and metaheuristic methods which are highly problem specific. In this work we describe the implementation of the Local Branching framework, originally developed for Mixed Integer Programming, in a CP-based environment. Constraint programming specific features are used to ease the search process, still mantaining an absolute generality of the approach. We also propose a search strategy called Sliced Neighborhood Search, SNS, that iteratively explores slices of large neighborhoods of an incumbent solution by performing CP-based tree search and encloses concepts from metaheuristic techniques. SNS can be used as a stand alone search strategy, but it can alternatively be embedded in existing strategies as intensification and diversification mechanism. In particular we show its integration within the CP-based local branching. We provide an extensive experimental evaluation of the proposed approaches on instances of the Asymmetric Traveling Salesman Problem and of the Asymmetric Traveling Salesman Problem with Time Windows. The proposed approaches achieve good results on practical size problem, thus demonstrating the benefit of integrating metaheuristic concepts in CP-based frameworks.
Resumo:
Timing of waiting list entrance for patients with cystic fibrosis in need of pulmonary transplant: the experience of a regional referral centre Objective: Evaluation of parameters that can predict a rapid decay of general conditions of patients affected by Cystic Fibrosis (CF) with no specific criteria to be candidate to pulmonary transplant. Material and methods: Fifteen patients with CF who died for complications and 8 who underwent lung transplantation in the 2000-2010 decade, were enrolled. Clinical data 2 years before the event (body max index, FEV1%, number of EV antibiotic treatments per year, colonization with Methicillin-resistant Staphylococcus aureus (MRSA), pseudomonas aeruginosa mucosus, burkholderia cepacia, pulmonary allergic aspergilosis) were compared among the 2 groups. Results: Mean FEV1% was significantly higher and mean number of antibiotic treatment was lower in deceased than in the transplanted patients (p<0.002 and p<0.001 respectively). Although in patients who died there were no including criteria to enter the transplant list 2 years before the exitus, suggestive findings such as low BMI (17.3), high incidence of hepatic pathology (33.3%), diabetes (50%), and infections with MRSA infection (25%), Pseudomonas aeruginosa (83.3%) and burkholderia cepacia (8.3%) were found with no statistical difference with transplanted patients, suggesting those patients were at risk of severe prognosis. In patients who died, females were double than males. Conclusion: While evaluating patients with CF, negative prognostic factors such as the ones investigated in this study, should be considered to select individuals with high mortality risk who need stricter therapeutical approach and follow up. Inclusion of those patients in the transplant waiting list should be taken into account.
Resumo:
This work presents exact algorithms for the Resource Allocation and Cyclic Scheduling Problems (RA&CSPs). Cyclic Scheduling Problems arise in a number of application areas, such as in hoist scheduling, mass production, compiler design (implementing scheduling loops on parallel architectures), software pipelining, and in embedded system design. The RA&CS problem concerns time and resource assignment to a set of activities, to be indefinitely repeated, subject to precedence and resource capacity constraints. In this work we present two constraint programming frameworks facing two different types of cyclic problems. In first instance, we consider the disjunctive RA&CSP, where the allocation problem considers unary resources. Instances are described through the Synchronous Data-flow (SDF) Model of Computation. The key problem of finding a maximum-throughput allocation and scheduling of Synchronous Data-Flow graphs onto a multi-core architecture is NP-hard and has been traditionally solved by means of heuristic (incomplete) algorithms. We propose an exact (complete) algorithm for the computation of a maximum-throughput mapping of applications specified as SDFG onto multi-core architectures. Results show that the approach can handle realistic instances in terms of size and complexity. Next, we tackle the Cyclic Resource-Constrained Scheduling Problem (i.e. CRCSP). We propose a Constraint Programming approach based on modular arithmetic: in particular, we introduce a modular precedence constraint and a global cumulative constraint along with their filtering algorithms. Many traditional approaches to cyclic scheduling operate by fixing the period value and then solving a linear problem in a generate-and-test fashion. Conversely, our technique is based on a non-linear model and tackles the problem as a whole: the period value is inferred from the scheduling decisions. The proposed approaches have been tested on a number of non-trivial synthetic instances and on a set of realistic industrial instances achieving good results on practical size problem.
Resumo:
The development of High-Integrity Real-Time Systems has a high footprint in terms of human, material and schedule costs. Factoring functional, reusable logic in the application favors incremental development and contains costs. Yet, achieving incrementality in the timing behavior is a much harder problem. Complex features at all levels of the execution stack, aimed to boost average-case performance, exhibit timing behavior highly dependent on execution history, which wrecks time composability and incrementaility with it. Our goal here is to restitute time composability to the execution stack, working bottom up across it. We first characterize time composability without making assumptions on the system architecture or the software deployment to it. Later, we focus on the role played by the real-time operating system in our pursuit. Initially we consider single-core processors and, becoming less permissive on the admissible hardware features, we devise solutions that restore a convincing degree of time composability. To show what can be done for real, we developed TiCOS, an ARINC-compliant kernel, and re-designed ORK+, a kernel for Ada Ravenscar runtimes. In that work, we added support for limited-preemption to ORK+, an absolute premiere in the landscape of real-word kernels. Our implementation allows resource sharing to co-exist with limited-preemptive scheduling, which extends state of the art. We then turn our attention to multicore architectures, first considering partitioned systems, for which we achieve results close to those obtained for single-core processors. Subsequently, we shy away from the over-provision of those systems and consider less restrictive uses of homogeneous multiprocessors, where the scheduling algorithm is key to high schedulable utilization. To that end we single out RUN, a promising baseline, and extend it to SPRINT, which supports sporadic task sets, hence matches real-world industrial needs better. To corroborate our results we present findings from real-world case studies from avionic industry.
Resumo:
Recent research has shown that the performance of a single, arbitrarily efficient algorithm can be significantly outperformed by using a portfolio of —possibly on-average slower— algorithms. Within the Constraint Programming (CP) context, a portfolio solver can be seen as a particular constraint solver that exploits the synergy between the constituent solvers of its portfolio for predicting which is (or which are) the best solver(s) to run for solving a new, unseen instance. In this thesis we examine the benefits of portfolio solvers in CP. Despite portfolio approaches have been extensively studied for Boolean Satisfiability (SAT) problems, in the more general CP field these techniques have been only marginally studied and used. We conducted this work through the investigation, the analysis and the construction of several portfolio approaches for solving both satisfaction and optimization problems. We focused in particular on sequential approaches, i.e., single-threaded portfolio solvers always running on the same core. We started from a first empirical evaluation on portfolio approaches for solving Constraint Satisfaction Problems (CSPs), and then we improved on it by introducing new data, solvers, features, algorithms, and tools. Afterwards, we addressed the more general Constraint Optimization Problems (COPs) by implementing and testing a number of models for dealing with COP portfolio solvers. Finally, we have come full circle by developing sunny-cp: a sequential CP portfolio solver that turned out to be competitive also in the MiniZinc Challenge, the reference competition for CP solvers.
Resumo:
A High-Performance Computing job dispatcher is a critical software that assigns the finite computing resources to submitted jobs. This resource assignment over time is known as the on-line job dispatching problem in HPC systems. The fact the problem is on-line means that solutions must be computed in real-time, and their required time cannot exceed some threshold to do not affect the normal system functioning. In addition, a job dispatcher must deal with a lot of uncertainty: submission times, the number of requested resources, and duration of jobs. Heuristic-based techniques have been broadly used in HPC systems, at the cost of achieving (sub-)optimal solutions in a short time. However, the scheduling and resource allocation components are separated, thus generates a decoupled decision that may cause a performance loss. Optimization-based techniques are less used for this problem, although they can significantly improve the performance of HPC systems at the expense of higher computation time. Nowadays, HPC systems are being used for modern applications, such as big data analytics and predictive model building, that employ, in general, many short jobs. However, this information is unknown at dispatching time, and job dispatchers need to process large numbers of them quickly while ensuring high Quality-of-Service (QoS) levels. Constraint Programming (CP) has been shown to be an effective approach to tackle job dispatching problems. However, state-of-the-art CP-based job dispatchers are unable to satisfy the challenges of on-line dispatching, such as generate dispatching decisions in a brief period and integrate current and past information of the housing system. Given the previous reasons, we propose CP-based dispatchers that are more suitable for HPC systems running modern applications, generating on-line dispatching decisions in a proper time and are able to make effective use of job duration predictions to improve QoS levels, especially for workloads dominated by short jobs.