Upgrade to Pro
— share decks privately, control downloads, hide ads and more …
Speaker Deck
Features
Speaker Deck
PRO
Sign in
Sign up for free
Search
Search
Software Transactional Memory
Search
Bucharest FP
February 25, 2016
Programming
380
0
Share
Embed
Copy iframe code
Copy JS code
Copy link
Start on current slide
Software Transactional Memory
Bucharest FP
February 25, 2016
More Decks by Bucharest FP
See All by Bucharest FP
The Curry-Howard-Lambek Correspondence
bucharestfp
3
980
An Applicative Application
bucharestfp
0
11k
Composition in FP
bucharestfp
0
400
Formal Design, Implementation and Verification of Blockchain Languages and Virtual Machines
bucharestfp
1
720
PureScript & Halogen
bucharestfp
1
470
A Simple Sudoku Solver in Haskell
bucharestfp
0
1.2k
DeviceGraph — Clustering Devices into People at Adobe with Apache Spark
bucharestfp
0
310
Functional Programming Inception
bucharestfp
0
450
Equational Reasoning in Programming
bucharestfp
0
1.1k
Other Decks in Programming
See All in Programming
コーディングルールの鮮度を保ちたい for SRE NEXT 2026 / keep-fresh-go-internal-conventions-sre-next-2026
handlename
0
140
yield再入門 #phpcon
o0h
PRO
0
480
音楽のための関数型プログラミング言語mimiumにおける多段階計算の活用
tomoyanonymous
1
330
Welcome to the "Parametricity" 🏙️ − Generic だけど Specific な世界 −
guvalif
PRO
1
170
『コードを書く以外の』エンジニアリング〜課金基盤移行プロジェクト推進のためのTips4選
yuriko1211
0
510
AI 輔助遺留系統現代化的經驗分享
jame2408
1
1.2k
ローカルLLMでどこまでコードが書けるか -拡張版 / How much code can be written on a local LLM Extended
kishida
12
4.8k
Prismを使った型安全な暗号化_関数型まつり2026
_fhhmm
0
140
型も通る、synthも通る、それでも危ない 〜AIのCDKの権限とコストを機械で検証する〜 / It Passes Type Checks, It Passes Synth Checks, but It’s Still Risky — Automatically Verifying Permissions and Costs in AI’s CDK —
seike460
PRO
1
360
PHPだって関数型したい 〜できること、できないこと〜 / fp-in-php
jsoizo
0
210
はてなアカウント基盤 State of the Union
cockscomb
1
1.3k
AIキャラアプリkaiwaの低遅延音声通話基盤をどう作ったか - AWS Gravitonで支える低遅延・低コストAI Agent基盤
mogamit
0
170
Featured
See All Featured
Applied NLP in the Age of Generative AI
inesmontani
PRO
4
2.4k
B2B Lead Gen: Tactics, Traps & Triumph
marketingsoph
0
170
Navigating Algorithm Shifts & AI Overviews - #SMXNext
aleyda
1
1.4k
Art, The Web, and Tiny UX
lynnandtonic
304
22k
Faster Mobile Websites
deanohume
310
32k
How to Grow Your eCommerce with AI & Automation
katarinadahlin
PRO
1
230
The Mindset for Success: Future Career Progression
greggifford
PRO
0
420
The Success of Rails: Ensuring Growth for the Next 100 Years
eileencodes
47
8.2k
The World Runs on Bad Software
bkeepers
PRO
72
12k
Lightning talk: Run Django tests with GitHub Actions
sabderemane
0
220
Visualization
eitanlees
152
17k
Chasing Engaging Ingredients in Design
codingconduct
0
240
Transcript
Software-Transactional Memory in Haskell (an overview of the implementation)
Let's start with WHY
FACT: Many modern applications have increasingly stringent concurrency requirements
FACT: Commodity multicore systems are increasingly affordable and available
FACT: The design and implementation of correct, efficient, and scalable
concurrent software remains a daunting task
Haskell to the rescue! Meet STM
STM protects shared state in concurrent programs
STM provides a more user-friendly and scalable alternative to locks
by promoting the notion of memory transactions as first-class citizens
Transactions, like many of the best ideas in computer science,
originated in the data engineering world
Transactions are one of the foundations of database technology
Full-fledged transactions are defined by the ACID properties Memory transactions
use two of them (A+I)
Transactions provide atomicity and isolation guarantees
Strong atomicity means all-or-nothing
Strong isolation means freedom from interference by other threads
Recall that Haskell is a strictly-typed, lazy, pure functional language
Pure means that functions with side-effects must be marked as
such
The marking is done through the type system at compile
time
STM is just another kind of I/O (with a different
marker: "STM a" instead of "IO a")
Transactional memory needs to be declared explicitly as TVar
The STM library provides an STM-to-IO converter called "atomically"
Transactional memory can only be accessed through dedicated functions like
"modifyTVar", "readTVar", "writeTVar" which can only be called inside STM blocks
Implementation Overview Of GHC's STM
Definition A transaction memory is a set of tuples in
the shape of (Identity,Version,Value) The version number represents the number of times the value has changed.
The Transactional Record Every STM transaction keeps a record of
state changes (similar to the tx log in the DB world)
STM performs all the effects of a transaction locally in
the transactional record
Once the transaction has finished its work locally, a version-based
consistency check determines if the values read for the entire access set are consistent
This version-based consistency check also obtains locks for the write
set and with those locks STM updates the main memory and then releases the locks
Rolling back the effects of a transaction means forgetting the
current transactional record and starting again
Reading: When a readTVar is attempted STM first searches the
tr. record for an existing entry
Reading: If the entry is found, STM will use that
local view of the TVar
Reading: On the first readTVar, a new entry is allocated
and the TVar value is read and stored locally
Reading: The original Tvar does not need to be accessed
again for its value until validation time
Writing: Writing to a Tvar requires that the variable first
be in the tr. record
Writing: If it is not currently in the tr. record,
a readTVar is performed and the value is stored in a new entry
Writing: The version in this entry will be used at
validation time to ensure that no updates were made concurrently to this TVar
Writing: The value is stored locally in the tr. record
until commit time
Validation: Before a transaction can make its effects visible to
other threads it must check that it has seen a consistent view of memory while it was executing
Validation: This is done by checking that TVars hold their
expected values (version comparison)
Validation: During validation, STM fetches the version numbers for all
TVars and checks that they are consistent with its expectations
Validation: STM then acquires locks for the write set in
ascending order of memory address
Validation: STM then reads and checks all version numbers again
Validation: If the version numbers are again consistent with its
expectations, STM allows the commit to happen
Committing: The desired atomicity is guaranteed by: • Validation having
witnessed all TVars with their respective expected values • Locks being held for all of the TVars in the write set
Committing: STM proceeds to increment each locked TVar's num_updates (a.k.a.
version) field
Committing: STM then writes the new values into the respective
current_value fields, and releases the locks
Committing: While these updates happen one-by-one, any attempt to read
from this set will spin while the lock is held
Another useful STM abstraction is the TChan, an unbounded FIFO
channel
Once some messages are transferred into a TChan, they are
ready to be consumed by other threads (broadcasting is possible too)
TChans are useful when threads need to send signals to
each other, as opposed to just accessing shared state
Compile your STM code with: ghc -threaded program.hs When running
the program: ./program +RTS -N
Follow me on GitHub github.com/dserban