Publication

Isolation-only Transactions by Typing and Versioning

2004
Reports

Abstract

In this paper we design a language and runtime support for isolation-only, multithreaded transactions (called tasks) that are intended for time-critical systems. The key concept of our design is the use of a type system to support rollback-free and safe runtime execution of tasks. We present a first-order type system which can verify information for the concurrency controller. We use an operational semantics to formalize and prove the type soundness result and an isolation property of tasks. The semantics uses a specialized concurrency control algorithm, that is based on access versioning. We give proofs of type soundness and dynamic correctness of the concurrency control algorithm.

Official source

https://infoscience.epfl.ch/entities/publication/41f9df3f-1e54-4a85-84c9-78904d2401db

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Graph Chat

Chat with Graph Search

Ask any question about EPFL courses, lectures, exercises, research, news, etc. or try the example questions below.

DISCLAIMER: The Graph Chatbot is not programmed to provide explicit or categorical answers to your questions. Rather, it transforms your questions into API requests that are distributed across the various IT services officially administered by EPFL. Its purpose is solely to collect and recommend relevant references to content that you can explore to help you answer your questions.

2004
Reports

Abstract

Official source

https://infoscience.epfl.ch/entities/publication/41f9df3f-1e54-4a85-84c9-78904d2401db

About this result

Related concepts (32)

Type system

In computer programming, a type system is a logical system comprising a set of rules that assigns a property called a type (for example, integer, floating point, string) to every "term" (a word, phrase, or other set of symbols). Usually the terms are various constructs of a computer program, such as variables, expressions, functions, or modules. A type system dictates the operations that can be performed on a term. For variables, the type system determines the allowed values of that term.

Type theory

In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general, type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that were proposed as foundations are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory. Most computerized proof-writing systems use a type theory for their foundation, a common one is Thierry Coquand's Calculus of Inductive Constructions.

Operational semantics

Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms (denotational semantics).

Related publications (32)

Isolation-only Transactions by Typing and Versioning

Chat with Graph Search

Scalable and Resource-Efficient Stream Processing

Interoperability of Proof Systems with SC-TPTP

The Fifth Typology: A Symposium on Type and Architecture