A proof system for lock-free concurrency

Dissertação para obtenção do Grau de Mestre em Engenharia Informática

Lock-free Parallel Dynamic Programming

We show a method for parallelizing top down dynamic programs in a straightforward way by a careful choice of a lock-free shared hash table implementation and randomization of the order in which the dynamic program computes its subproblems. This generic approach is applied to dynamic programs for knapsack, shortest paths, and RNA structure alignment, as well as to a state-of-the-art solution for minimizing the máximum number of open stacks. Experimental results are provided on three different modern multicore architectures which show that this parallelization is effective and reasonably scalable. In particular, we obtain over 10 times speedup for 32 threads on the open stacks problem.

Formalising progress properties of non-blocking programs

A non-blocking program is one that uses non-blocking primitives, such as load-linked/store-conditional and compare-and-swap, for synchronisation instead of locks so that no process is ever blocked. According to their progress properties, non-blocking programs may be classified as wait-free, lock-free or obstruction-free. However, a precise description of these properties does not exist and it is not unusual to find a definition that is ambiguous or even incorrect. We present a formal definition of the progress properties so that any confusion is removed. The formalisation also allows one to prove the widely believed presumption that wait-freedom is a special case of lock-freedom, which in turn is a special case of obstruction-freedom.

Disseny i implementació d'una web administrable i d'una aplicació per dispositius mòbils

En la societat en què vivim cada vegada agafen més importància les pàgines web, ja que és una eina d’informació molt útil i ràpida de consultar. Per això, no s’entén que una activitat empresarial sigui del tipus que sigui, no tingui representació a la xarxa. No és necessari que l’activitat en qüestió hagi de vendre productes a través d’Internet, sinó que simplement aquesta representació pot ajudar a donar a conèixer l’empresa i a ampliar la cartera de clients. De la mateixa manera, els dispositius mòbils també s’estan convertint en una eina important en la societat d’avui en dia i una bona aplicació pot aportar-te un avantatge en moltes de les feines diàries de les persones. D’aquestes idees sorgeix el projecte de fer la web i l’aplicació pel centre de fisioteràpia Fisioripoll. La web serviria per tenir un lloc a la xarxa on donar-se a conèixer i poder captar nous clients, i l’aplicació funcionaria com a eina pel propi centre, seria una espècie d’agenda electrònica per saber les hores que tens reservades els pròxims dies. Per aconseguir un bon funcionament de la web, s’ha demanat que la pàgina sigui administrable en els seus continguts. És a dir, que els propis gestors del centre puguin canviar els texts, les imatges dels diferents apartats i gestionar les reserves dels clients. En canvi, l’aplicació serà només una eina de consulta i no s’hauria de gestionar res. Per tal de dur a terme aquesta web s’ha tingut en compte utilitzar eines de programació de distribució lliure com és el llenguatge PHP, la base de dades MySQL, jQuery, el framework Phonegap per tal de poder construir una web i una aplicació amb cost de programari nul.

Disseny i implementació d'una web administrable i d'una aplicació per dispositius mòbils

En la societat en què vivim cada vegada agafen més importància les pàgines web, ja que és una eina d’informació molt útil i ràpida de consultar. Per això, no s’entén que una activitat empresarial sigui del tipus que sigui, no tingui representació a la xarxa. No és necessari que l’activitat en qüestió hagi de vendre productes a través d’Internet, sinó que simplement aquesta representació pot ajudar a donar a conèixer l’empresa i a ampliar la cartera de clients. De la mateixa manera, els dispositius mòbils també s’estan convertint en una eina important en la societat d’avui en dia i una bona aplicació pot aportar-te un avantatge en moltes de les feines diàries de les persones. D’aquestes idees sorgeix el projecte de fer la web i l’aplicació pel centre de fisioteràpia Fisioripoll. La web serviria per tenir un lloc a la xarxa on donar-se a conèixer i poder captar nous clients, i l’aplicació funcionaria com a eina pel propi centre, seria una espècie d’agenda electrònica per saber les hores que tens reservades els pròxims dies. Per aconseguir un bon funcionament de la web, s’ha demanat que la pàgina sigui administrable en els seus continguts. És a dir, que els propis gestors del centre puguin canviar els texts, les imatges dels diferents apartats i gestionar les reserves dels clients. En canvi, l’aplicació serà només una eina de consulta i no s’hauria de gestionar res. Per tal de dur a terme aquesta web s’ha tingut en compte utilitzar eines de programació de distribució lliure com és el llenguatge PHP, la base de dades MySQL, jQuery, el framework Phonegap per tal de poder construir una web i una aplicació amb cost de programari nul.

Improvements in Hardware Transactional Memory for GPU Architectures

In the multi-core CPU world, transactional memory (TM)has emerged as an alternative to lock-based programming for thread synchronization. Recent research proposes the use of TM in GPU architectures, where a high number of computing threads, organized in SIMT fashion, requires an effective synchronization method. In contrast to CPUs, GPUs offer two memory spaces: global memory and local memory. The local memory space serves as a shared scratch-pad for a subset of the computing threads, and it is used by programmers to speed-up their applications thanks to its low latency. Prior work from the authors proposed a lightweight hardware TM (HTM) support based in the local memory, modifying the SIMT execution model and adding a conflict detection mechanism. An efficient implementation of these features is key in order to provide an effective synchronization mechanism at the local memory level. After a quick description of the main features of our HTM design for GPU local memory, in this work we gather together a number of proposals designed with the aim of improving those mechanisms with high impact on performance. Firstly, the SIMT execution model is modified to increase the parallelism of the application when transactions must be serialized in order to make forward progress. Secondly, the conflict detection mechanism is optimized depending on application characteristics, such us the read/write sets, the probability of conflict between transactions and the existence of read-only transactions. As these features can be present in hardware simultaneously, it is a task of the compiler and runtime to determine which ones are more important for a given application. This work includes a discussion on the analysis to be done in order to choose the best configuration solution.

Hiord: A type-free higher-order logic programming language with predicate abstraction

A new formalism, called Hiord, for defining type-free higherorder logic programming languages with predicate abstraction is introduced. A model theory, based on partial combinatory algebras, is presented, with respect to which the formalism is shown sound. A programming language built on a subset of Hiord, and its implementation are discussed. A new proposal for defining modules in this framework is considered, along with several examples.

Free expanding cloud of cold atoms as an atomic standard: Ramsey fringes contrast

A compact frequency standard based on an expanding cold (133)CS cloud is under development in our laboratory. In a first experiment, Cs cold atoms were prepared by a magneto-optical trap in a vapor cell, and a microwave antenna was used to transmit the radiation for the clock transition. The signal obtained from fluorescence of the expanding cold atoms cloud is used to lock a microwave chain. In this way the overall system stability is evaluated. A theoretical model based on a two-level system interacting with the two microwave pulses enables interpretation for the observed features, especially the poor Ramsey fringes contrast. (C) 2008 Optical Society of America.

Derivative-free nonlinear optimization filter simplex

The filter method is a technique for solving nonlinear programming problems. The filter algorithm has two phases in each iteration. The first one reduces a measure of infeasibility, while in the second the objective function value is reduced. In real optimization problems, usually the objective function is not differentiable or its derivatives are unknown. In these cases it becomes essential to use optimization methods where the calculation of the derivatives or the verification of their existence is not necessary: direct search methods or derivative-free methods are examples of such techniques. In this work we present a new direct search method, based on simplex methods, for general constrained optimization that combines the features of simplex and filter methods. This method neither computes nor approximates derivatives, penalty constants or Lagrange multipliers.

Characterizations of power indices based on null player free winning coalitions

In this paper, we characterize two power indices introduced in [1] using two different modifications of the monotonicity property first stated by [2]. The sets of properties are easily comparable among them and with previous characterizations of other power indices.

Direct search optimization application programming interface with remote access

Search Optimization methods are needed to solve optimization problems where the objective function and/or constraints functions might be non differentiable, non convex or might not be possible to determine its analytical expressions either due to its complexity or its cost (monetary, computational, time,...). Many optimization problems in engineering and other fields have these characteristics, because functions values can result from experimental or simulation processes, can be modelled by functions with complex expressions or by noise functions and it is impossible or very difficult to calculate their derivatives. Direct Search Optimization methods only use function values and do not need any derivatives or approximations of them. In this work we present a Java API that including several methods and algorithms, that do not use derivatives, to solve constrained and unconstrained optimization problems. Traditional API access, by installing it on the developer and/or user computer, and remote API access to it, using Web Services, are also presented. Remote access to the API has the advantage of always allow the access to the latest version of the API. For users that simply want to have a tool to solve Nonlinear Optimization Problems and do not want to integrate these methods in applications, also two applications were developed. One is a standalone Java application and the other a Web-based application, both using the developed API.

Web-based application programming interface to solve nonlinear optimization problems

Nonlinear Optimization Problems are usual in many engineering fields. Due to its characteristics the objective function of some problems might not be differentiable or its derivatives have complex expressions. There are even cases where an analytical expression of the objective function might not be possible to determine either due to its complexity or its cost (monetary, computational, time, ...). In these cases Nonlinear Optimization methods must be used. An API, including several methods and algorithms to solve constrained and unconstrained optimization problems was implemented. This API can be accessed not only as traditionally, by installing it on the developer and/or user computer, but it can also be accessed remotely using Web Services. As long as there is a network connection to the server where the API is installed, applications always access to the latest API version. Also an Web-based application, using the proposed API, was developed. This application is to be used by users that do not want to integrate methods in applications, and simply want to have a tool to solve Nonlinear Optimization Problems.

Dynamic programming for a Markov-switching jump–diffusion

We consider an optimal control problem with a deterministic finite horizon and state variable dynamics given by a Markov-switching jump–diffusion stochastic differential equation. Our main results extend the dynamic programming technique to this larger family of stochastic optimal control problems. More specifically, we provide a detailed proof of Bellman’s optimality principle (or dynamic programming principle) and obtain the corresponding Hamilton–Jacobi–Belman equation, which turns out to be a partial integro-differential equation due to the extra terms arising from the Lévy process and the Markov process. As an application of our results, we study a finite horizon consumption– investment problem for a jump–diffusion financial market consisting of one risk-free asset and one risky asset whose coefficients are assumed to depend on the state of a continuous time finite state Markov process. We provide a detailed study of the optimal strategies for this problem, for the economically relevant families of power utilities and logarithmic utilities.

A Modular Programming Approach for IoTBased Wireless Sensor Networks

Poster presented in 12th European Conference on Wireless Sensor Network (EWSN 2015). 9 to 11, Feb, 2015. Porto, Portugal.

Data-centric concurrency control on the java programming language

Dissertação para obtenção do Grau de Mestre em Engenharia Informática