* LSFMMBPF proposal [General/MM]: SRCU: a case study in memory ordering
@ 2023-01-11 14:43 Joel Fernandes
0 siblings, 0 replies; 2+ messages in thread
From: Joel Fernandes @ 2023-01-11 14:43 UTC (permalink / raw)
To: lsf-pc
Cc: Boqun Feng, Frederic Weisbecker, Paul E. McKenney,
Steven Rostedt, linux-mm, rcu
Title: SRCU: a case study in memory ordering
Description:
Memory ordering guarantees are the backbone of SRCU, an important RCU
synchronization mechanism in the kernel. Can we use the Linux kernel
memory model to understand complex concurrent code better?
In this talk, we will go over:
- SRCU internals overview and why it works
- Discuss in detail, all the 8 or so memory barriers in SRCU and why
they are needed.
- Comparable access patterns to each barrier (LB, MP etc)
- Linux kernel memory model (LKMM) experiments on studying effects of
each memory barrier, along with execution candidate graphs generated
by herd7.
- Possible formal methods / models.
- Discuss both correctness and forward progress issues tackled by
these memory barriers.
(Resending as my previous email got messed up by mail client, thanks).
- Joel
^ permalink raw reply [flat|nested] 2+ messages in thread
* LSFMMBPF proposal [General/MM]: SRCU: a case study in memory ordering
@ 2023-01-11 11:32 Joel Fernandes
0 siblings, 0 replies; 2+ messages in thread
From: Joel Fernandes @ 2023-01-11 11:32 UTC (permalink / raw)
To: lsf-pc
Cc: Boqun Feng, Frederic Weisbecker, Paul E. McKenney,
Steven Rostedt, linux-mm, rcu
[-- Attachment #1: Type: text/plain, Size: 741 bytes --]
Title: SRCU: a case study in memory ordering
Description:
Memory ordering guarantees are the backbone of SRCU, an important RCU
synchronization mechanism in the kernel. Can we use the Linux kernel memory
model to understand complex concurrent code better?
In this talk, we will go over:
- SRCU internals overview and why it works
- in detail, all the 8 or so memory barriers in SRCU and why they are
needed.
- comparable access patterns to each barrier (LB, MP etc)
- Linux kernel memory model (LKMM) experiments on studying effects of each
memory barrier, along with execution candidate graphs generated by herd7.
- possible formal methods / models.
- discuss both correctness and forward progress issues tackled by these
memory barriers
[-- Attachment #2: Type: text/html, Size: 1007 bytes --]
^ permalink raw reply [flat|nested] 2+ messages in thread
end of thread, other threads:[~2023-01-11 14:43 UTC | newest]
Thread overview: 2+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-01-11 14:43 LSFMMBPF proposal [General/MM]: SRCU: a case study in memory ordering Joel Fernandes
-- strict thread matches above, loose matches on Subject: below --
2023-01-11 11:32 Joel Fernandes
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox