Preventing atomicity violations with contracts

Concurrent programming is a difficult and error-prone task because the programmer must reason about multiple threads of execution and their possible interleavings. A concurrent program must synchronize the concurrent accesses to shared memory regions, but this is not enough to prevent all anomalies that can arise in a concurrent setting. The programmer can misidentify the scope of the regions of code that need to be atomic, resulting in atomicity violations and failing to ensure the correct behavior of the program. Executing a sequence of atomic operations may lead to incorrect results when these operations are co-related. In this case, the programmer may be required to enforce the sequential execution of those operations as a whole to avoid atomicity violations. This situation is specially common when the developer makes use of services from third-party packages or modules. This thesis proposes a methodology, based on the design by contract methodology, to specify which sequences of operations must be executed atomically. We developed an analysis that statically verifies that a client of a module is respecting its contract, allowing the programmer to identify the source of possible atomicity violations.

Análise de complexidade de programas em ferramentas de apoio à decisão

Dissertação de mestrado em Engenharia de Sistemas

Disseny d'una eina de suport a la reutilització de codi

Aquest projecte tracta sobre el desenvolupament d'una eina de suport a la reutilització de codi de programació. L'eina té com a objectiu augmentar la productivitat dels desenvolupadors per mitjà de la reutilització de codi. Per facilitar la reutilització l'eina proposa un sistema jeràrquic on el codi de programació i la diferent informació sobre aquest es guarden en anotacions, les anotacions formen part d'una pàgina i els conjunts de pàgines són organitzats en projectes.

Característiques dels Generadors de Codi

Aquest estudi permet tenir una visió de les possibilitats reals dels generadors de codi, les seves característiques més destacades i les seves mancances. Finalment s'inclou una proposta de millora per incorporar als generadors de codi.

Anàlisi i comparativa de frameworks dins de les 3 capes (Vista-Model-Dades) d'una arquitecturatípica JEE

Analitzarem, mitjançant proves de codi que realitzen la mateixa tasca, dels diferentsFramework escollits, la seva eficiència (velocitat i memòria entre d'altres).

Gestión de expedientes para ayuntamientos

Aplicació web que pot ser desplegada en qualsevol contenidor d'aplicacions JAVA, sigui o no "FULL-compliant" J2EE. Mostra com amb molt poc codi s'aconsegueix una aplicació que té gestió d'usuaris, permisos, expedients, etcètera. Fins i tot s'ha inclòs la funcionalitat d'emmagatzemar / recuperar fitxers a la base de dades.

J2EE : Generació automàtica de codi

Aquest projecte està enfocat a determinar l'estat actual de les principals eines de generació automàtica de codi que existeixen, analitzant les característiques principals de cada eina determinar-ne les funcionalitats.

Diseño e implementación de un framework de persistencia

Los Frameworks constituyen el nuevo paradigma en cuanto al desarrollo de software se refiere. Entre sus principales características se encuentran la facilidad para la reutilización de código. En este marco específico proporcionados por la tecnología usaremos la tecnología JAVA y su extensión en cuanto a la persistencia de datos. El Framework de persistencia es el responsable de gestionar la lógica de acceso a los datos en un SGBD (Sistema de Gestión de Bases de Datos), ya sea de entrada o salida, y ocultando los detalles más pesados relativos a la estructura propia de la Base de Datos utilizada, de manera completa y transparentemente. En conclusión, este proyecto se basa en un análisis del los Frameworks existentes, analizando sus características y profundizando en los detalles concretos de su actividad y manejo en cuanto a la persistencia.

Retirement Investors' Club Plan Document; 401 (a) Employer Match Plan, 2005

This Plan is intended to be a qualified plan within the meaning of Code Section 401(a), a plan within the meaning of Code Section 401(a), and a governmental plan within the meaning of Code Section 414(d). This Plan may be referred to as “The State of Iowa’s 401(a) Employer Match Plan”, which is one of two plans that comprise the Retirement Investors’ Club (RIC).

Iowa Flood Mitigation Board Annual Report, 2015

The Iowa Flood Mitigation Program is created within Code of Iowa, Chapter 418. The Program seeks to provide funds for fl ood mitigation projects that otherwise would not be funded. The Flood Mitigation Board is responsible for the implementation of Code of Iowa Chapter 418. The membership of the Board is comprised of four voting public members appointed by the Governor, five voting members representing state agencies, four non-voting ex officio members of the legislature, and one non-voting ex officio member representing a state agency.

Data Collection Agent Framework

Ohjelmistoteollisuudessa pitkiä ja vaikeita kehityssyklejä voidaan helpottaa käyttämällä hyväksi ohjelmistokehyksiä (frameworks). Ohjelmistokehykset edustavat kokoelmaa luokkia, jotka tarjoavat yleisiä ratkaisuja tietyn ongelmakentän tarpeisiin vapauttaen ohjelmistokehittäjät keskittymään sovelluskohtaisiin vaatimuksiin. Hyvin suunniteltujen ohjelmistokehyksien käyttö lisää suunnitteluratkaisujen sekä lähdekoodin uudelleenkäytettävyyttä enemmän kuin mikään muu suunnittelulähestymistapa. Tietyn kohdealueen tietämys voidaan tallentaa ohjelmistokehyksiin, joista puolestaan voidaan erikoistaa viimeisteltyjä ohjelmistotuotteita. Tässä diplomityössä kuvataan ohjelmistoagentteihin (software agents) perustuvaa ohjelmistokehyksen suunnittelua toteutusta. Pääpaino työssä on vaatimusmäärittelyä vastaavan suunnitelman sekä toteutuksen kuvaaminen ohjelmistokehykselle, josta voidaan erikoistaa erilaiseen tiedonkeruuseen kykeneviä ohjelmistoja Internet ympäristöön. Työn kokeellisessa osuudessa esitellään myös esimerkkisovellus, joka perustuu työssä kehitettyyn ohjelmistokehykseen.

Matalakompleksisen palvelupyyntömallin kehittäminen palveluväylää hyödyntäviin järjestelmäintegraatioihin

Tässä työssä kehitetään yleiskäyttöinen palvelupyyntömalli, jonka avulla Lahden kaupungin Lahti Fenix –projektin Kuntalaistilijärjestelmän palveluväylän kautta voidaan kutsua järjestelmän tietokantatasoa tai muita palveluväylän avulla integroituja järjestelmiä. Työn tavoitteena oli suoraviivaistaa järjestelmäintegraatioihin liittyvien palveluiden kehittämistä suunnittelemalla sellainen palvelupyyntömuodostin, joka ei sisällä staattisia viittauksia jossakin tietyssä palvelussa käytettäviin luokkiin tai muihin ominaisuuksiin. Työssä hyödynnettiin Java-kielen kehittyneitä ominaisuuksia; reflektiivistä ohjelmointia, geneeristä ohjelmointia ja Java-virtuaalikoneen metodipinon lukemista. Tavoitteen saavuttamista mitattiin käyttäen avuksi McCaben syklomaattista kompleksisuutta ja metodeissa käytettyä rivimäärää. Työ aloitettiin joulukuussa 2008 ja saatiin valmiiksi helmikuussa 2009. Työn tuloksena syntyi toimiva, syklomaattiselta kompleksisuudeltaan matala ja helppokäyttöinen palvelukutsumuodostin.

Building object-oriented software with the D-Bus messaging system

Object-oriented programming is a widely adopted paradigm for desktop software development. This paradigm partitions software into separate entities, objects, which consist of data and related procedures used to modify and inspect it. The paradigm has evolved during the last few decades to emphasize decoupling between object implementations, via means such as explicit interface inheritance and event-based implicit invocation. Inter-process communication (IPC) technologies allow applications to interact with each other. This enables making software distributed across multiple processes, resulting in a modular architecture with benefits in resource sharing, robustness, code reuse and security. The support for object-oriented programming concepts varies between IPC systems. This thesis is focused on the D-Bus system, which has recently gained a lot of users, but is still scantily researched. D-Bus has support for asynchronous remote procedure calls with return values and a content-based publish/subscribe event delivery mechanism. In this thesis, several patterns for method invocation in D-Bus and similar systems are compared. The patterns that simulate synchronous local calls are shown to be dangerous. Later, we present a state-caching proxy construct, which avoids the complexity of properly asynchronous calls for object inspection. The proxy and certain supplementary constructs are presented conceptually as generic object-oriented design patterns. The e ect of these patterns on non-functional qualities of software, such as complexity, performance and power consumption, is reasoned about based on the properties of the D-Bus system. The use of the patterns reduces complexity, but maintains the other qualities at a good level. Finally, we present currently existing means of specifying D-Bus object interfaces for the purposes of code and documentation generation. The interface description language used by the Telepathy modular IM/VoIP framework is found to be an useful extension of the basic D-Bus introspection format.

Readout architectures for hybrid pixel detector readout chips

The original contribution of this thesis to knowledge are novel digital readout architectures for hybrid pixel readout chips. The thesis presents asynchronous bus-based architecture, a data-node based column architecture and a network-based pixel matrix architecture for data transportation. It is shown that the data-node architecture achieves readout efficiency 99% with half the output rate as a bus-based system. The network-based solution avoids “broken” columns due to some manufacturing errors, and it distributes internal data traffic more evenly across the pixel matrix than column-based architectures. An improvement of > 10% to the efficiency is achieved with uniform and non-uniform hit occupancies. Architectural design has been done using transaction level modeling (TLM) and sequential high-level design techniques for reducing the design and simulation time. It has been possible to simulate tens of column and full chip architectures using the high-level techniques. A decrease of > 10 in run-time is observed using these techniques compared to register transfer level (RTL) design technique. Reduction of 50% for lines-of-code (LoC) for the high-level models compared to the RTL description has been achieved. Two architectures are then demonstrated in two hybrid pixel readout chips. The first chip, Timepix3 has been designed for the Medipix3 collaboration. According to the measurements, it consumes < 1 W/cm^2. It also delivers up to 40 Mhits/s/cm^2 with 10-bit time-over-threshold (ToT) and 18-bit time-of-arrival (ToA) of 1.5625 ns. The chip uses a token-arbitrated, asynchronous two-phase handshake column bus for internal data transfer. It has also been successfully used in a multi-chip particle tracking telescope. The second chip, VeloPix, is a readout chip being designed for the upgrade of Vertex Locator (VELO) of the LHCb experiment at CERN. Based on the simulations, it consumes < 1.5 W/cm^2 while delivering up to 320 Mpackets/s/cm^2, each packet containing up to 8 pixels. VeloPix uses a node-based data fabric for achieving throughput of 13.3 Mpackets/s from the column to the EoC. By combining Monte Carlo physics data with high-level simulations, it has been demonstrated that the architecture meets requirements of the VELO (260 Mpackets/s/cm^2 with efficiency of 99%).

Equational Reasoning about Object-Oriented Programs

Formal verification of software can be an enormous task. This fact brought some software engineers to claim that formal verification is not feasible in practice. One possible method of supporting the verification process is a programming language that provides powerful abstraction mechanisms combined with intensive reuse of code. In this thesis we present a strongly typed functional object-oriented programming language. This language features type operators of arbitrary kind corresponding to so-called type protocols. Sub classing and inheritance is based on higher-order matching, i.e., utilizes type protocols as basic tool for reuse of code. We define the operational and axiomatic semantics of this language formally. The latter is the basis of the interactive proof assistant VOOP (Verified Object-Oriented Programs) that allows the user to prove equational properties of programs interactively.