Rely-guarantee protocols for safe interference over shared memory

Mutable state can be useful in certain algorithms, to structure programs, or for efficiency purposes. However, when shared mutable state is used in non-local or nonobvious ways, the interactions that can occur via aliases to that shared memory can be a source of program errors. Undisciplined uses of shared state may unsafely interfere with local reasoning as other aliases may interleave their changes to the shared state in unexpected ways. We propose a novel technique, rely-guarantee protocols, that structures the interactions between aliases and ensures that only safe interference is possible. We present a linear type system outfitted with our novel sharing mechanism that enables controlled interference over shared mutable resources. Each alias is assigned separate, local roles encoded in a protocol abstraction that constrains how an alias can legally use that shared state. By following the spirit of rely-guarantee reasoning, our rely-guarantee protocols ensure that only safe interference can occur but still allow many interesting uses of shared state, such as going beyond invariant and monotonic usages. This thesis describes the three core mechanisms that enable our type-based technique to work: 1) we show how a protocol models an alias’s perspective on how the shared state evolves and constrains that alias’s interactions with the shared state; 2) we show how protocols can be used while enforcing the agreed interference contract; and finally, 3) we show how to check that all local protocols to some shared state can be safely composed to ensure globally safe interference over that shared memory. The interference caused by shared state is rooted at how the uses of di↵erent aliases to that state may be interleaved (perhaps even in non-deterministic ways) at run-time. Therefore, our technique is mostly agnostic as to whether this interference was the result of alias interleaving caused by sequential or concurrent semantics. We show implementations of our technique in both settings, and highlight their di↵erences. Because sharing is “first-class” (and not tied to a module), we show a polymorphic procedure that enables abstract compositions of protocols. Thus, protocols can be specialized or extended without requiring specific knowledge of the interference produce by other protocols to that state. We show that protocol composition can ensure safety even when considering abstracted protocols. We show that this core composition mechanism is sound, decidable (without the need for manual intervention), and provide an algorithm implementation.

Consistent state software transactional memory

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para a obtenção do Grau de Mestre em Engenharia Informática

Diagnosis of an EPS module

Dissertação apresentada na Faculdade de Ciências e Tecnologia da Universidade Nova de Lisboa para obtenção do grau de Mestre em Engenharia Electrotécnica e Computadores

The state of environmental performance evaluation in the public sector: the case of the Portuguese defence sector

Journal of Cleaner Production, nº 17, p. 36-52

Introduction: Guinea-Bissau Today - The Irrelevance of the State and the Permanence of Change

African Studies Review, Volume 52, Number 2, pp. 35–

Hybrid link-state path-vector protocol ++

Dissertação para obtenção do Grau de Mestre em Engenharia Electrotécnica e de Computadores Mestrado Integrado em Engenharia Electrotécnica e de Computadores

Development and implementation of strategies for the incorporation of reinforcing elements in aluminium alloys by solid state processing

Dissertação para obtenção do Grau de Mestre em Engenharia Mecânica

Islamic reformism in India between 1857 and 1947: the conception of state in Chiragh ‘Ali, Muhammad Iqbal and Sayyid Abu’l ‘Ala Mawdudi

Tese apresentada para cumprimento dos requisitos necessários à obtenção do grau de Doutor em Ciência Política, especialidade de Teoria e Análise Política.

Spatial and temporal analysis of recent drought using vegetation temperature condition index: case of Somali regional state of Ethiopia

Dissertation submitted in partial fulfillment of the requirements for the Degree of Master of Science in Geospatial Technologies.

THE U.S. and European M&A cycles: A Markov switching and state space approach

A Work Project, presented as part of the requirements for the Award of a Masters Degree in Finance from the NOVA – School of Business and Economics

Structural characterization of the urea-unfolded state of Colicin Immunity Protein Im7 and Im9

Dissertação para obtenção do Grau de Mestre em Bioquímica Estrutural e Funcional

Digestão anaeróbia de resíduos agroalimentares: reutilização das frações líquidas e sólidas (state-of-art)

Dissertação para obtenção do Grau de Mestre em Energia e Bioenergia

Air lime-earth blended mortars - Assessment on fresh state and workability

International Conference on Vernacular Heritage, Sustainability and Earthen Architecture, VerSus 2014, 2nd MEDITERRA, 2nd ResTAPIA, 11-13 September, Valencia, Spain

State detection in a financial portfolio: a self-organizing maps approach for financial time series

This study analyses financial data using the result characterization of a self-organized neural network model. The goal was prototyping a tool that may help an economist or a market analyst to analyse stock market series. To reach this goal, the tool shows economic dependencies and statistics measures over stock market series. The neural network SOM (self-organizing maps) model was used to ex-tract behavioural patterns of the data analysed. Based on this model, it was de-veloped an application to analyse financial data. This application uses a portfo-lio of correlated markets or inverse-correlated markets as input. After the anal-ysis with SOM, the result is represented by micro clusters that are organized by its behaviour tendency. During the study appeared the need of a better analysis for SOM algo-rithm results. This problem was solved with a cluster solution technique, which groups the micro clusters from SOM U-Matrix analyses. The study showed that the correlation and inverse-correlation markets projects multiple clusters of data. These clusters represent multiple trend states that may be useful for technical professionals.

Functional MRI of stimulus interference on auditory processing in normal listeners and tinnitus patients

We are constantly immersed in stimuli. Upon reaching our senses, stimuli are processed within various brain systems along various pathways into the brain, and eventually turned into a percept. However, there are percepts that do not result from responses to external source stimuli. A particular case of this situation is the auditory percept known as tinnitus. Tinnitus can be seen as a task-irrelevant auditory percept, commonly reported to interfere with normal daily tasks. This is known from reports made by tinnitus sufferers that refer to their phantom percept as distracting, and that it diverts their focus from the task-relevant stimuli.(...)