Publications

Export 53 results:
Sort by: Author [ Title  (Asc)] Type Year
A B C D E F G H I J K L M N O P Q R S T U V W X Y Z 
P
Pessanha, V., "Practical Verification of Anomalies in Transactional Memory Programs", FCT - Universidade Nova de Lisboa: Universidade Nova de Lisboa, 2011. Abstract2011-vasco_pessanha.pdf

Transactional Memory (TM) is an approach to concurrency control in general pur- pose programming languages that inherits the concept of transaction from the database setting. Unlike other language constructs such as locks, TM has an optimistic approach to concurrency control by allowing more than one thread to access simultaneously the same critical section. A transaction always executes as if it is alone in the system, and in the end its effects are undone (rolled back) if it conflicts with another concurrent transac- tions. In spite of the potential for increasing scalability and performance, TM is a recent and developing programming model and still has a very limited impact in real-world applications.
Designing and developing concurrent software is difficult and error prone. Concur- rent programs exhibit concurrency anomalies that originate faults and failures. Despite some claims that TM programs are less error prone, they still exhibit concurrency anoma- lies such as high-level dataraces, i.e., wrong delimitations of transactions’ scope, and stale-value errors, that occur when the value of a shared variable jumps from an atomic block to another.
Programs with this kind of anomalies can exhibit unpredictable and wrong behaviour, not fulfilling the goals for which they were conceived.
This work aims the detection of anomalies through static analysis of transactional Java ByteCode programs that execute in strong atomicity. A extensible and flexible framework is proposed, which can be extended with plugins that detect specific types of anomalies. With this framework we expect to prove that high-level dataraces and stale-value errors can be detected with reasonable precision through static analysis.

Keywords: Atomicity Violation, High-Level Datarace, Static Analysis, Concurrency, Software Transactional Memory

Pessanha, V., R. J. Dias, J. M. Lourenço, E. Farchi, and D. Sousa, "Practical verification of high-level dataraces in transactional memory programs", Proceedings of 9th the Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, New York, NY, USA, ACM, pp. 26–34, July, 2011. Abstract2011-padtad.pdf

In this paper we present MoTh, a tool that uses static analysis to enable the automatic verification of concurrency anomalies in Transactional Memory Java programs. Currently MoTh detects high-level dataraces and stale-value errors, but it is extendable by plugging-in sensors, each sensor implementing an anomaly detecting algorithm. We validate and benchmark MoTh by applying it to a set of well known concurrent buggy programs and by close comparison of the results with other similar tools. The results achieved so far are very promising, yielding good accuracy while triggering only a very limited number of false warnings.

Dias, R. J., V. Pessanha, and J. M. Lourenço, "Precise Detection of Atomicity Violations", Hardware and Software: Verification and Testing, vol. 7857: Springer Berlin / Heidelberg, pp. 8-23, 2013. Abstract2012-hvc.pdf

n/a

Sousa, D. G., C. Ferreira, and J. M. Lourenço, "Prevenção de Violações de Atomicidade usando Contractos", Proceedings of INForum Simpósio de Informática, Lisbon, Portugal, Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa, pp. 190–201, sep, 2013. Abstract2013-inforum-ds.pdf

n/a

Sousa, D. G., "Preventing atomicity violations with contracts", Universidade Nova de Lisboa, 2013. 2013-diogo_sousa.pdf
Sousa, D., J. M. Lourenço, C. Ferreira, and R. J. Dias, Preventing Atomicity Violations with Contracts, , no. UNL-2014: Faculdade de Ciências e Tecnologia, Universidade Nova de Lisboa, 2014. Abstract2014-sousa.pdf

n/a

Q
Simão, J., and L. Veiga, "QoE-JVM: An Adaptive and Resource-Aware Java Runtime for Cloud Computing", On the Move to Meaningful Internet Systems: OTM 2012, vol. 7566: Springer Berlin / Heidelberg, pp. 566-583, 2012. Abstract2012._qoe-jvm_doa.pdf

Cloud computing has been dominated by system-level virtual machines to enable the management of resources using a coarse grained approach, largely in a manner independent from the applications running on these infrastructures. However, in such environments, although different types of applications can be running, the resources are often delivered in a equal manner to each one, missing the opportunity to manage the available resources in a more efficient and application aware or driven way. Our proposal is QoE-JVM supporting Java applications with a global and elastic distributed image of a high-level virtual machine (HLLVM), where total resource consumption and allocation (within and across applications in the infrastructure) are driven by incremental gains in quality-of-execution (QoE), which relates the resources allocated to an application and the performance the application can extract from having those resources. In this paper, we discuss how critical resources (memory and CPU) can be allocated among HLL-VMs, so that Cloud providers can exchange resource slices among virtual machines, continually adaptdressing where those resources are required, while being able to determine where the reduction will be more economically effective, i.e., will contribute in lesser extent to performance degradation.

Simão, J., and L. {\'ıs Veiga, "QoE-JVM: An Adaptive and Resource-Aware Java Runtime for Cloud Computing", 2nd International Symposium on Secure Virtual Infrastructures (DOA-SVI 2012), OTM Conferences 2012: Springer, LNCS, sep, 2012. Abstract2012-doa-simao.pdf

n/a

R
Rameshan, N., and L. Veiga, "RATS - Resource Aware Thread Scheduling for JVM-level Clustering", INFORUM 2012 - Simpósio de Informática, sep, 2012. Abstractinforum-2012-navaneeth.pdf

n/a

Martins, H. R. L., J. Soares, J. M. Lourenço, and N. Preguiça, "Replicação Multi-nível de Bases de Dados em Memória", Proceedings of INForum Simpósio de Informática, Lisbon, Portugal, Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa, pp. 190–201, sep, 2013. Abstract2013-inforum-hm.pdf

n/a

Silva, J. A., T. M. Vale, J. M. Lourenço, and H. Paulino, "Replicação Parcial com Memória Transacional Distribuída", Proceedings of INForum Simpósio de Informática, Lisbon, Portugal, Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa, pp. 310–321, 2013. Abstract2013-inforum-js.pdf

n/a

Silva, J. P. M., and L. {\'ıs Veiga, "Reprodução Probabilística de Execuções na JVM em Multi-processadores", INFORUM 2012 - Simpósio de Informática, sep, 2012. Abstractinforum-2012-jpsilva-replay.pdf

n/a

Simão, J., N. Rameshan, and L. Veiga, "Resource-Aware Scaling of Multi-threaded Java Applications in Multi-tenancy Scenarios", IEEE CloudCom 2013: IEEE, dec, 2013. Abstract2013-cloudcom-simao-b.pdf

n/a

Pina, L., L. Veiga, and M. Hicks, "Rubah: DSU for Java on a stock JVM", ACM Conference on Object-Oriented Programming Languages, Systems, and Applications (OOPSLA 2014): ACM, sep, 2014. Abstract2014-oopsla-pina-core-a.pdf

n/a

S
Dias, R. J., D. Distefano, J. M. Lourenço, and J. C. Seco, StarTM: Automatic Verification of Snapshot Isolation in Transactional Memory Java Programs, , no. UNL-DI-6-2011, Lisboa, Departamento de Informática FCT/UNL, 2011. Abstractddls11.pdf

This paper presents StarTM , an automatic verification tool for transactional memory Java programs executing under relaxed isolation levels. We certify which transactions in a program are safe to execute under Snapshot Isolation without triggering the write-skew anomaly, opening the way to run-time optimizations that may lead to considerable performance enhancements.
Our tool builds on a novel shape analysis technique based on Separation Logic to statically approximate the read- and write-sets of a transactional memory Java program. This technique is particularly challenging due to the presence of dynamically allocated memory.
We implement our technique and apply our tool to a set of intricate examples. We corroborate known results, certifying some of the examples for safe execution under Snapshot Isolation by proving the absence of write-skew anomalies. In other cases we identify transactions that potentially trigger the write-skew anomaly.

Luís, J. E., J. M. Lourenço, and P. A. Lopes, "Suporte Transaccional para o Sistema de Ficheiros Btrfs", InForum 2011: Proceedings of InForum Simpósio de Informática, Coimbra, Universidade do Coimbra, 2011. Abstract2011-inforum-jel.pdf2011-inforum-short-jel.pdf

Em caso de falha abrupta de um sistema, é imperativo garantir a consistência do Sistema de Ficheiros (SF). Actualmente existem várias solu{\c c}ões que visam garantir que tanto os dados como os metadados do SF se encontram num estado consistente, mas que não contemplam a garantia de consistência dos dados do ponto de vista das aplica{\c c}ões. Por exemplo, aplica{\c c}ões que pretendam alterar vários ficheiros de configura{\c c}ão terão de encontrar mecanismos para garantir que, ou todos os ficheiros são devidamente alterados, ou nenhum o é, evitando assim que numa situa{\c c}ão de falha o conteúdo dos ficheiros fique inconsistente. Do ponto de vista da aplica{\c c}ão, pode não ser simples implementar este comportamento sobre um SF t{\'ıpico; e pode também não ser razoável utilizar um Sistema de Gestão de Bases de Dados (SGBD), que oferece propriedades ACID. Neste artigo propomos, testamos e avaliamos uma integra{\c c}ão das propriedades ACID num SF. Partindo do suporte para snapshots do sistema de ficheiros Btrfs, oferece-se uma semântica transaccional às aplica{\c c}ões que operam sobre volumes (sub-árvores) do SF, sem comprometer a semântica POSIX do SF.

Silva, J. A., T. M. Vale, R. J. Dias, H. Paulino, and J. M. Lourenço, "Supporting Multiple Data Replication Models in Distributed Transactional Memory", Proceedings of the 2015 International Conference on Distributed Computing and Networking, Goa, India, ACM, 2015. Abstract2015-icdcn.pdf

n/a

T
Sampaio, P., P. Ferreira, and L. Veiga, "Transparent scalability with clustering for Java e-science applications", Proceedings of the 11th IFIP WG 6.1 international conference on Distributed applications and interoperable systems, Berlin, Heidelberg, Springer-Verlag, pp. 270–277, 2011. Abstract2011-dais-sampaio.pdf

The two-decade long history of events relating object-oriented programming, the development of persistence and transactional support, and the aggregation of multiple nodes in a single-system image cluster, appears to convey the following conclusion: programmers ideally would develop and deploy applications against a single shared global memory space (heap of objects) of mostly unbounded capacity, with implicit support for persistence and concurrency, transparently backed by a possibly large number of clustered physical machines.

In this paper, we propose a new approach to the design of OODB systems for Java applications: (O3)2 (pronounced ozone squared). It aims at providing to developers a single-system image of virtually unbounded object space/heap with support for object persistence, object querying, transactions and concurrency enforcement, backed by a cluster of multi-core machines with Java VMs that is kept transparent to the user/developer. It is based on an existing persistence framework (ozone-db) and the feasibility and performance of our approach has been validated resorting to the OO7 benchmark.

Vale, T., and R. J. Dias, TribuSTM Instrumentation Rules, , Lisboa, Departamento de Informática FCT/UNL, 2012. tribustm_instrumentation_rules.pdf
Luís, J. E., "TxBtrfs — A Transactional Snapshot-based File System", FCT - Universidade Nova de Lisboa: Universidade Nova de Lisboa, 2011. Abstract2011-joao_luis.pdf

Several decades ago, the file system was the container of choice for large bulks of related information, kept in hundreds of files, and relying on applications specifically created to handle them. These configurations weren't scalable and could easily become difficult to maintain, leading to the development and adoption of Database Management Systems (DBMS). These systems, capable of efficiently handling vast amounts of data, allowed heavy concurrency without requiring the programmer to deal with concurrency-control mechanisms, by encapsulating operations within transactions.
The properties of Transactions rapidly became an object of desire by many, and efforts to bring them to general-purpose programming environments began. In recent years there have been breakthroughs in bringing the transactional semantics to memory, using Software Transactional Memory (STM), providing abstractions to concurrency-control on the application-level. However, STM failed to meet some expectations, specially regarding I/O operations, forcing the abstraction to go deeper in the system: directly to the file system.
In this document we shall discuss file systems in general, their properties and common structure, although focusing in those with transactional or versioning capabilities. Later on, we will present our proposed enhancement of an existing Linux file system (Btrfs), in order to offer transactional semantics to applications, while detecting potential conflicts between concurrent flows of execution and reconciling their changes whenever possible.

U
Vale, T. M., R. J. Dias, and J. M. Lourenço, "Uma Infraestrutura para Suporte de Memória Transacional Distribuída", Proceedings of INForum Simpósio de Informática, Lisbon, Portugal, Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa, pp. 177–189, 2012. Abstract2012-inforum-tv.pdf

As técnicas e algoritmos desenvolvidos sobre diferentes infraestruturas específicas dificilmente podem ser comparados entre si. Este princípio também se aplica às infraestruturas para execução de Memória Transacional Distribuída (MTD), pois não só são muito escassas aquelas que permitem o desenvolvimento, teste e comparação de vários algoritmos e técnicas de implementação, como fornecem uma interface intrusiva para o programador. Sem uma comparação justa, não é possível aferir quais as técnicas e algoritmos mais apropriados em cada contexto de utilização (workload). Neste artigo propomos uma infraestrutura generalista, muito flexível, que possibilita a experimentação de várias estratégias de MTD, permitindo o desenvolvimento de uma grande variedade de algoritmos e de técnicas de implementação eficientes e otimizadas. Através da sua utilização, é agora possível a comparação de técnicas e algoritmos em diferentes contextos de utilização (workloads), recorrendo a uma única infraestrutura e com implicações mínimas no código da aplicação.

Vale, T. M., R. J. Dias, and J. M. Lourenço, "Uma Infraestrutura para Suporte de Memória Transacional Distribuída", Proceedings of INForum Simpósio de Informática, Lisbon, Portugal, Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa, pp. 177–189, sep, 2012. Abstract2012-inforum-tv.pdf

n/a

Farchi, E., I. Segall, J. M. Lourenço, and D. G. Sousa, "Using Program Closures to Make an Application Programming Interface (Api) Implementation Thread Safe", Proceedings of the 2012 Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, Minneapolis, MN, USA, ACM, pp. 18–24, 2012. Abstract2012-padtad.pdf

Consider a set of methods implementing an Application Programming Interface (API) of a given library or program module that is to be used in a multithreaded setting. If those methods were not originally designed to be thread safe, races and deadlocks are expected to happen. This work introduces the novel concept of program closure and describes how it can be applied in a methodology used to make the library or module implementation thread safe, by identifying the high level data races introduced by interleaving the parallel execution of methods from the API. High-level data races result from the misspecification of the scope of an atomic block, by wrongly splitting it into two or more atomic blocks sharing a data dependency. Roughly speaking, the closure of a program P, clos(P), is obtained by incrementally adding new threads to P in such a way that enables the identification of the potential high level data races that may result from running P in parallel with other programs. Our model considers the methods implementing the API of a library of program module as concurrent programs and computes and analyses their closure in order to identify high level data races. These high level data races are inspected and removed to make the interface thread safe. We illustrate the application of this methodology with a simple use case.