Publications

Export 53 results:
Sort by: Author Title [ Type  (Desc)] Year
Book Chapter
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

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.

Dias, R. J., D. Distefano, J. C. Seco, and J. M. Lourenço, "Verification of Snapshot Isolation in Transactional Memory Java Programs", ECOOP 2012 – Object-Oriented Programming, vol. 7313, Beijing, China, Springer Berlin Heidelberg, pp. 640-664, 2012. Abstract2012-ecoop.pdf

This paper presents an automatic verification technique for transactional memory Java programs executing under snapshot isolation level. 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 work builds on a novel deep-heap analysis technique based on separation logic to statically approximate the read- and write-sets of a transactional memory Java program. We implement our technique and apply our tool to a set of micro benchmarks and also to one benchmark of the STAMP package. 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 our analysis has identified transactions that potentially trigger previously unknown write-skew anomalies.