Serializability Enforcement for Concurrent ML

Duration: 1 hour 4 mins 39 secs

Share this media item:

Embed this media item:

<iframe width="_width_" height="_height_" src="https://sms.cam.ac.uk/media/852567/embed" frameborder="0" scrolling="no" allowfullscreen></iframe>

Choose size:

About this item

Available Formats

About this item

Description:	http://www.talks.cam.ac.uk/talk/index/19191


Created:	2010-06-10 11:12
Collection:	Computer Laboratory Wednesday Seminars
Publisher:	University of Cambridge
Copyright:	Computer Laboratory
Language:	eng (English)


Abstract:	There has been much recent interest in exploring higher-level concurrency control abstractions such as software transactional memory (STM) to alleviate the complexity of reasoning about interactions among concurrent threads of control. Isolation and atomicity are the two critical properties provided by an STM that guarantee serializability of concurrent actions. Isolation ensures that transactions execute without interference from effects performed by other transactions, and atomicity guarantees that intermediate effects performed by a transaction are not seen by other concurrently executing transactions. While STM has been mostly studied in the context of shared-memory concurrency, the atomicity and isolation properties it provides can benefit message-passing systems as well. In this talk, we explore the integration of these features into Concurrent ML, a dialect of ML that supports first-class synchronous message-based communication events. Central to our design is the introduction of an isolate, a combinator that ensures its argument events, which may be arbitrarily complex, execute concurrently with strong isolation guarantees. In conjunction with an orthogonal combinator that provides atomicity, we achieve a programming model that fully integrates transactional support into a CML -style concurrency model, resulting in improved expressivity and safety. We also present an overview of an implementation in MLton, a whole-program optimizing compiler for ML.

Abstract:

There has been much recent interest in exploring higher-level concurrency control abstractions such as software transactional memory (STM) to alleviate the complexity of reasoning about interactions among concurrent threads of control. Isolation and atomicity are the two critical properties provided by an STM that guarantee serializability of concurrent actions. Isolation ensures that transactions execute without interference from effects performed by other transactions, and atomicity guarantees that intermediate effects performed by a transaction are not seen by other concurrently executing transactions.

While STM has been mostly studied in the context of shared-memory concurrency, the atomicity and isolation properties it provides can benefit message-passing systems as well. In this talk, we explore the integration of these features into Concurrent ML, a dialect of ML that supports first-class synchronous message-based communication events. Central to our design is the introduction of an isolate, a combinator that ensures its argument events, which may be arbitrarily complex, execute concurrently with strong isolation guarantees. In conjunction with an orthogonal combinator that provides atomicity, we achieve a programming model that fully integrates transactional support into a CML -style concurrency model, resulting in improved expressivity and safety. We also present an overview of an implementation in MLton, a whole-program optimizing compiler for ML.

Available Formats

Format	Quality	Bitrate	Size
MPEG-4 Video	480x360	1.84 Mbits/sec	894.12 MB	View	Download
WebM	480x360	602.9 kbits/sec	282.61 MB	View	Download
Flash Video	480x360	804.22 kbits/sec	381.30 MB	View	Download
Flash Video	320x240	435.72 kbits/sec	206.59 MB	View	Download
iPod Video	480x360	505.25 kbits/sec	239.55 MB	View	Download
MP3	44100 Hz	125.03 kbits/sec	59.07 MB	Listen	Download
Auto *	(Allows browser to choose a format it supports)