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.

A cenografia oitocentista como fonte de cultura visual e de ideologia

A argumentação centra-se na história da produção cenográfica da segunda metade do século XIX em Portugal, propondo um tratamento teórico mais abrangente, que desloque o enfoque analítico da peça de arte em si ou do carácter efémero e global da espectacularidade que tem merecido alguma atenção da historiografia contemporânea, para uma escala de cultura visual ou mesmo de visualidade, no sentido mais dilatado destas expressões. Discutindo essencialmente a problemática em torno da imagem teatral como produto do mundo oitocentista analisa-se o potencial cognitivo da série cenográfica na sua capacidade de representação e apropriações ideológicas. Para esta dialéctica concorrem as repercussões epocais do espectáculo, designadamente na regulação da vida social, na mediação de processos económicos, no combate político, e sobretudo, em modelos de percepção artística fundados nos convencionalismos cenográficos como acontece, por exemplo, na produção decorativa e arquitectónica integradas num particular campo visual ou na teatralidade actuante dos edifícios, cuja essência, em todos os casos, é devedora de uma cultura paradoxalmente centrada nos limites da caixa cénica e na infinitude emotiva do espectacular.

Visual politics of the estado novo realized on the Alameda Dom Afonso Henriques in Lisbon – the construction of ideal citizenship?

The stylistic categorization of the Estado Novo has been intensely discussed by Portuguese art historians. The square Alameda Dom Afonso Henriques in Lisbon (Alameda) can be seen as paradigmatic for the architecture of power of the Estado Novo. The Alameda forms a gardened valley between two hills. There you find two prominent and highly propagandist buildings: The Instituto Superior Técnico (IST) and the Fonte Luminosa are dedicated to modern sciences and respectively to the harmonious contribution of nature to the city. The iconography of the Alameda as well as its incorporation into the propagandist use of urban planning in the 1930s and 1940s exemplify the visual politics during Salazarism. Urban planning programs intended to create cities that would preserve the character of a traditional catholic society and at the same time answer to the need to modernize the country and evoke the image of a progressive state. Thus, public buildings and urban squares such as the Alameda contributed to design a corporate image and to the ‘spirit’ of the regime.

Shared lives social impact bond feasibility study

Loneliness and isolation among the elderly is an enormous problem in Portugal. Interventions to tackle loneliness worldwide have had limited success, and new approaches are needed. Shared Lives is an adult foster placement service in the UK that shows significant promise in tackling both loneliness, isolation and other societal challenges linked with ageing. This feasibility study suggests that replicating a Shared Lives service in Portugal, using a Social Impact Bond (SIB), is viable and likely to create both social and financial value for all stakeholders involved. This study provides recommendations for how a Shared Lives SIB could be designed and implemented.