Marco Aldinucci, Dynamic shared data in structured parallel programming frameworks

Abstract. This work originates from the wish to simplify the coding of irregular applications within structured parallel programming environments. In these environments parallelism is exploited by composing "skeletons", i.e. parallelism exploitation patterns. The skeletal approach has been proved to be effective, at least if application algorithms can be somehow expressed in terms of skeleton composition. However, in some cases our skeletal frameworks fail in providing the application programmer with convincing solutions both from ease of programming and performance viewpoints. Major lacks of expressivity have emerged in dynamic/irregular algorithms and applications that oddly access to large data sets. The first part of the thesis moves along this path, and reports all attempts we made to improve the effectiveness of environments' compiler, static optimizer, and run-time support.
The main goal of the thesis is to take a step further with respect to the achieved results. In particular we aim to defeat expressivity lacks emerged in skeletal languages approaching irregular problems and dealing with dynamic data structures. The basic idea consists in providing the application designer with a shared address space and a skeletal framework that enables and enforces the co-design of (shared) dynamic data structures and (parallel) algorithms.
At this aim, a new skeletal programming environment based on shared address programming is proposed (i.e. eskimo). The language is as an extension of a "host" language (i.e. the C language). eskimo is conceived to be a framework to experiment how to support dynamic data structures in a skeletal framework. Its run-time support is based on a software distributed shared memory, and allows the programmer to freely access data items in the shared memory. eskimo is designed to match the hooks offered by ASSIST, thus to be experimented within. Notably eskimo is not yet another DSM, rather it relies on DSM already known technologies to experiment the co-design of dynamic data structures and parallel programming patterns enforcing locality in the distributed memory access.
eskimo has been designed and developed from scratch. eskimo run-time support exploits multithreading, dynamic data-driven scheduling, and is very tolerant with respect to standard POSIX programming framework. It will be released as open source package. [gzipped postscript]

Andrea Bracciali, Behavioural patterns and software composition

Abstract. The way in which we conceive of software is substantially changing and our current experience of the digital world is based on distributed environments, populated by applications which consist of components interacting with each other, and tend to be distributed over different domains, if not moving throughout them. Other than computational skills, the success of an application depends even more on the capability of its components to successfully coordinate their tasks.
In this thesis we concentrate on the definition of a formal model to describe and verify the composition of the interactive behaviours of components. This study is motivated by the necessity to coordinate components, which are autonomous in their behaviours, and need to cooperate in an environment which may be only partially specified and subject to timely changes, since it is dynamically evolving, and possibly even populated by hostile components trying to exploit the work of the others.
Starting from a simplified name-passing calculus, we extend traditional component interfaces with behavioural descriptions, define the mechanisms by means of which components can be connected together, and characterise the open environment where they interact. A notion of correctness is defined for open environments and an algorithmic procedure for its verification is provided. Components spoiling the correctness of the system are not admitted. To release the last constraint, a methodology to adapt and hence accept components with mismatching behaviours is provided.
The framework fully supports the verification of security protocols, when they are seen as a composition of principals in an open environment subject to malicious components. A complete methodology for formalising and verifying security protocols is presented.
[gzipped postscript]

Valentina Ciriani, Three-Level Logic Synthesis: Algebraic Approach and Minimization Algorithms

Abstract. We address some problems arising in the synthesis of Boolean functions, in particular we study the minimization of EXOR-AND-OR networks called Sum of Pseudoproducts (SPP) forms. Recently introduced, three-level logic SPP forms allowed the representation of Boolean functions with much shorter expressions than standard two-level Sum of Products (SOP) expressions, or other three-level logic forms~\cite{LP99}. On the other hand SPP networks have a cumbersome theory, their minimization time is high, and the unbounded fan-in EXOR gates in SPP expressions are not easily implementable in the current technology. Consequently the main aims of this thesis are: $1$) rephrasing SPP theory in a well-known algebraic context to obtain an easier description of the networks; $2$) introducing much faster algorithms for SPP synthesis; $3$) defining new models of SPP networks with bounded fan-in EXOR gates, or bounded number of EXOR gates, whose minimization time is strongly reduced and whose minimal forms are still very compact; $4$) exploiting regularities of the input function in order to decrease the minimization complexity. We obtain these goals in two different ways, corresponding to the two parts of this thesis. The results of the first part are twofold. First we give a new algebraic description of SPP forms using affine spaces. This understanding of the theory allows us to describe a new canonical representation leading to more compact and efficient data structures for the minimization algorithms. Then we describe new SPP forms with bounded fan-in gates corresponding to practical networks, and for which the minimization time is drastically reduced. In the second part we study ``regularities'' of Boolean functions to decrease their minimization time. We attain several results. The regularity of a Boolean function $f$ of $n$ variables is expressed by its \emph{autosymmetry degree} $k$ (with $0 \le k\le n$), where $k=0$ means no regularity (that is, we are not able to provide any advantage over standard synthesis). For $k\geq 1$ the function is {\em autosymmetric}, and a new function $f_k$ is identified in polynomial time; $f_k$ is ``equivalent'' to, but smaller than $f$, and depends on $n-k$ variables only. Given a minimal SPP form for $f_k$, a minimal SPP form for $f$ is built in linear time. We also describe a new EXOR-AND-OR form, called ORAX, for autosymmetric functions. ORAX networks are a trade-off between SPP and SOP forms. Experimental results show that a large percentage of functions in the classical \textsc{Espresso} benchmark suite are autosymmetric, and the SPP minimization time is critically reduced for them.
[gzipped postscript]

Antonio Cisternino, Multi-stage and Meta-programming Support in Strongly Typed Execution Engines

Abstract. Program development and execution involves a number of processing and transformation steps performed by a variety of tools such as: preprocessors, compilers, program development environments, parser generators, software installers, operating system loaders, just to mention the most common ones. Each system takes as input a program in source or object form and produces a new program, which can be used as input to another system. This thesis develops a technique suitable to express staged computations, targeted to modern execution environments, such as the JVM and the CLR. Code fragments are introduced in programs as first class values, which can be composed by means of an operator called Bind. We discuss power of this opera-tor showing that it is type-safe and complete: only type sound code fragments can be generated; all possible programs can be produced from a finite set of base code fragments. Binding provides meta-programming support in the run-time environment. We show that the staging operators of MetaML can be ex-pressed in term of our mechanism. Implementation and performance issues are discussed for Bind and code values, i.e. the values representing code fragments. An execution model for programs based on the mechanism is proposed. A program is executed not only at runtime: a program evaluator may evaluate it at different times of its lifetime (after compilation, during installation, and so on). A distinctive feature of the model is that program transformations before runtime can be expressed in the program itself.
[gzipped postscript]

Ruggero Lanotte, An automaton-theoretic approach to safety and security in real-time systems

Abstract. Hybrid Systems are automata equipped with variables. Constraints on these variables are expressed by Mathematical Logics. Hybrid Systems are used for modeling embedded systems and time dependent processes. In these branches of study safety and security are among the main requirements that a system must satisfy, hence the interest of ways to express and prove these properties. The aim of the thesis is to extend the classical classes of Hybrid Systems and to study safety and security properties of real life systems. For this purpose, we consider different subclasses of High Order Mathematical Logics over real variables, integers variables, arrays with infinite elements and parameters. We recall four classes which are enclosed in First Order Mathematical Logics and for which the satisfiability problem of a formula is known to be decidable. We consider two new classes of High Order Mathematical Logics, where arrays can be quantified, and we prove decidability results of satisfiability. Then we define the classes of Hybrid Systems which have constraints expressed by the subclasses of Mathematical Logic mentioned above. For these systems we prove expressiveness results, and we show that reachability and invariant properties are semi-decidable. We give an algorithm based on predicate transformation to compute predecessor steps and successor steps of a given set of states. As an application we study safety in a temperature control system and in a web browser. To study security properties we define a Timed Information Flow Logic. We give an algorithm, which may not terminate, for verifying whether a Hybrid System satisfies a formula expressed in this logic. Moreover, we prove a decidability result for this problem if a special class of Hybrid Systems and formulas expressed in Timed Information Flow Logic are considered. As an example we model a problem of web privacy.
[gzipped postscript]

Eda Marchetti, Software testing in the XXI century: methods, tools and new approaches to manage, control and evaluate this critical phase

Abstract. Software Testing is a critical part of the whole process of development, on which the quality of the products delivered strictly depends. In this Thesis we present our journey through the world of Software Testing, ranging over many fields from definition to organization, from its applicability to analysis of its effectiveness, because testing activity is not limited to the detection of "bugs". The general aims are proposing both a global view of the testing phase, which exploits and unifies the knowledge from the industrial reality and the research context and putting research in practice. For this, starting from test planning we analyze the different testing stages pointing out their characteristic problems and presenting our original proposals (methods, tools or new approaches based on UML specifications) for solving them. In particular we also define procedural strategies, which support suitable testing choices since the first phases of development, and provide the reader with practical and quantitative guidance all along the testing phase. All the proposals presented are the result of a strict collaboration with software developers looking for solutions for their problems and improvements in the different activities of the testing process. This collaboration imposes us two important constraints: usability, i.e. the methodologies as far as possible must adapt themselves to the modelling notations and procedures commonly used by industries and real environments and not vice versa; and automation, i.e., increasing as much as possible the mechanization in test cases derivation, execution and validation, consequently reducing the manual labour. We adopt therefore the leading principle of providing readers with some easy-to-apply and low-cost methodologies, which maximize the automation and minimize as much as possible the required additional formalism or ad-hoc effort specifically for testing purposes. Moreover for completeness' sake for each topic treated we provide both a detailed survey of the literature, useful for knowing the state of the art and for comparing our solutions with those provided by the research world, and the evaluation of the methods proposed by means of case studies also taken from a real industrial context.
[gzipped postscript]

Alessio Micheli, Recursive Processing of Structured Domains in Machine Learning

Abstract. The adaptive processing of structured information (e.g. sequences, trees, graphs) is an emerging and critical topic in current Machine Learning research. In this thesis we propose the study of methods that are based on recursive functions for the adaptive transduction from structured domains, basically in the area of Neural Networks. Specifically, the neural computing realization of this approach, i.e. Recursive Neural Networks, deals with prediction tasks for patterns belonging to a structured domain, allowing a combination of the flexibility and the robustness of connectionist models with the representational power of a structured domain in a learning system.
Exploiting this basic idea, we propose new models, analysis of theoretical properties and applications aimed at extending the potentialities of the recursive neural computing approach in the Machine Learning framework.
A family of models, based on the Recursive Cascade Correlation methodology, is introduced to deal with contextual information in structured domains, allowing the extension of the traditional causality assumption. The proposed models allow us to realize contextual transductions and to extend, with respect to the causal models, the class of functions that can be computed for direct acyclic positional graphs. The computational power of the new contextual models is assessed both theoretically and experimentally.
The extension of the recursive dynamics to the unsupervised learning paradigm allows the formulation of a general framework for self-organizing maps able to cover previous approaches in literature. We offer a uniform formalism for studying the training mechanisms, the theoretical properties and the extensions to alternative new recursive-based unsupervised methods.
Finally, the adaptive recursive approach is exploited to develop a novel methodology for scientific applications in the area of computational Chemistry, offering a new perspective to the research in drug design and in the discovery of new compounds. The aim is to develop a general and flexible method for QSPR/QSAR (Quantitative Structure-Property Relationship and Quantitative Structure-Activity Relationship) analysis and to assess the recursive approach in real-world applications. Experimental results show the efficacity of the proposed approach for coping with heterogeneous data and problems.
[gzipped postscript]

Emilio Tuosto, Non-Functional Aspects of Wide Area Network Programming

Abstract. Wide-Area Network (WAN) applications have become one of the most popular applications in current distributed computing. Internet and the World Wide Web are now the primary environment for designing, developing and distributing applications. This scenario imposes different programming metaphors with respect to traditional applications. Theoretical models for formally reasoning on WAN applications must consider many crucial aspects and their mutual relationships, e.g. mobility, network awareness, security, service level agreement, etc. This dissertation attempts to formally define declarative approaches for dealing with various facets of actual WAN programming and verification issues. We propose a declarative approach based on hypergraphs that provide foundational framework for ``declaring'' components' behaviours of a distributed system. It is exercised with two well-known models for distributed computations as Ambient and Klaim. Moreover, we extend Klaim with constructs for specifying, at application level, network connections and related Quality of Service (QoS) requirements. It is also shown how a suitable translation of our Klaim extension into hypergraphs can be exploited for detecting and reserving optimal routing path with respect to the QoS constraints imposed by applications. We also introduce a process calculus and a logic that specifies a formal framework for declaring security protocols and properties. By means of symbolic verification technique, the framework can be exploited as a verification environment for model checking security protocols. The declarative flavour of the analysis and the ability of dealing with multi-session verification is the major advantage of the proposed approach. Finally, we describe a verification environment based on a semantic minimization algorithm for pi-calculus agents presented in co-algebraic setting. The final part of this dissertation introduces and discusses an implementation of the algorithm together with other verification facilities of the framework. A proofs that shows the correctness of the implementation with respect to the co-algebraic specification is given.
[gzipped postscript]

Ph.D. Theses of 2003