- Tc - mailweb.openeuler.org

答复: [Dev] TC双周例会
by liyongqiang 10 Oct '22

10 Oct '22

当前已收到议题： 1、审视22.09中的SPR feature包含KABI change的部分合并到22.03 SP1 ---- Intel Arch SIG: Jason Zeng/Jun Tian 欢迎大家继续申报议题~ -----原始约会----- 发件人: openEuler conference <public(a)openeuler.org> 发送时间: 2022年10月9日 17:12 收件人: openEuler conference; dev@openeuler.org,tc@openeuler.org 主题: [Dev] TC双周例会时间: 2022年10月12日星期三 10:00-12:00(UTC+08:00) 北京，重庆，香港特别行政区，乌鲁木齐。地点: 您好！ TC SIG 邀请您参加 2022-10-12 10:00 召开的Zoom会议(自动录制) 会议主题：TC双周例会会议内容：技术委员会双周例会，欢迎大家申报议题会议链接：https://us06web.zoom.us/j/86334837029?pwd=ZXZpV25Rc3N2ZytYZXdxTEpJbkJjUT09 会议纪要：https://etherpad.openeuler.org/p/TC-meetings 温馨提醒：建议接入会议后修改参会人的姓名，也可以使用您在gitee.com的ID 更多资讯尽在：https://openeuler.org/zh/ Hello! openEuler TC SIG invites you to attend the Zoom conference(auto recording) will be held at 2022-10-12 10:00, The subject of the conference is TC双周例会, Summary: 技术委员会双周例会，欢迎大家申报议题 You can join the meeting at https://us06web.zoom.us/j/86334837029?pwd=ZXZpV25Rc3N2ZytYZXdxTEpJbkJjUT09. Add topics at https://etherpad.openeuler.org/p/TC-meetings. Note: You are advised to change the participant name after joining the conference or use your ID at gitee.com. More information: https://openeuler.org/en/

1 0

Re: [Dev] sig-SDS双周例会纪要
by liuqinfei 27 Sep '22

27 Sep '22

2022年9月27日 sig-SDS 双周例会纪要与会者（gitee id）: SKY-池信泽(chixinze), 统信-杨晓亮(yangxiaoliang), 麒麟-滕磊, 麒麟-杨昭, 陆华成, 华为-张峰, 华为-陈续强, 华为-罗日新(rosinL), 华为-戴志威(DaiZhiwei), 华为-王增亮(wangzengliang), 华为-孙榕棋, 华为-刘秦飞(liuqinfei) 会议纲要社区需求进展(all) crimson特性评估和使能(罗日新)：验证rbd的随机读写，通过vstart启动，做crimson与classic OSD的性能对比解决了一些稳定性问题，已经提PR到上游社区，后端引擎已经可以正常执行开发patch实现集群多节点部署功能 ceph NOF方案卸载客户端开销(刘秦飞) 分享卸载方案，待后续推动解决开销优化、性能瓶颈等问题通过调整librbd线程数和绑核，单个rbd性能提升较多，但是扩展性不佳正在优化librbd的函数热点和falsesharing问题社区issue清理 openEuler22.03编译ceph16.2.7失败待进一步分析如何通过提patch将修复固化下来 ceph-deploy 适配openEuler 22.03 LTS 已经合入主线，待推动合入openEuler22.03 ceph容器化部署的支持使用麒麟提供的包，已经可以支持容器化部署 openEuler待升级podman以支持部署 podman升级3.3.4已经合入master，待合入22.03-LTS ceph rgw压缩加密特性增强（戴志威） UADK文档正在整理中，如果有需求可以向作者索取 ceph编译效率优化（陈续强）优化内容将在博客中分享（代码优化待投入）遗留问题梳理必要需支持的ceph版本，在openEuler上面做验证（滕磊）正在梳理需求版本，待兼顾社区需求确定需要支持的版本；制定分级支持ceph版本（全量验证、基本验证、未验证）的里程碑（刘秦飞）待输入项；跟踪openEuler 22.03LTS podman升级到3.3.4 （王增亮） -- Best regards, Qinfei 在 2022-09-26 16:00:50，"openEuler conference" <public(a)openeuler.org> 写道： >您好！ > >sig-SDS SIG 邀请您参加 2022-09-27 09:30 召开的Zoom会议(自动录制) > >会议主题：sig-SDS双周例会 > >会议内容： >1，社区需求进展（all） >2，社区issue进展 >3，ceph rgw压缩加密特性增强（戴志威） >4，ceph编译效率优化（陈续强） > >会议链接：https://us06web.zoom.us/j/82164150332?pwd=K3NoYXhvbVBKRFhQTTcwbG0rMmxaQT09 > >会议纪要：https://etherpad.openeuler.org/p/sig-SDS-meetings > >温馨提醒：建议接入会议后修改参会人的姓名，也可以使用您在gitee.com的ID > >更多资讯尽在：https://openeuler.org/zh/ > > > > >Hello! > >openEuler sig-SDS SIG invites you to attend the Zoom conference(auto recording) will be held at 2022-09-27 09:30, > >The subject of the conference is sig-SDS双周例会, > >Summary: >1，社区需求进展（all） >2，社区issue进展 >3，ceph rgw压缩加密特性增强（戴志威） >4，ceph编译效率优化（陈续强） > >You can join the meeting at https://us06web.zoom.us/j/82164150332?pwd=K3NoYXhvbVBKRFhQTTcwbG0rMmxaQT09. > >Add topics at https://etherpad.openeuler.org/p/sig-SDS-meetings. > >Note: You are advised to change the participant name after joining the conference or use your ID at gitee.com. > >More information: https://openeuler.org/en/ >

1 0

[PATCH] Memory model: Fix the memory model issues for Linux kernel
by Hanjun Guo 24 Sep '22

24 Sep '22

From: Jonas Oberhauser <jonas.oberhauser(a)huawei.com> This is the update and fixes for memory model, simplify the model by removing redundancies, making semantics of seq-cst explicit, making ppo a subset of po, making ppo locally computable, as well as eliminating several spurious bugs in qspinlock and litmus tests, and ensuring correct compilation to the official power model. These issues were detected by Jonas Oberhauser, Viktor Vafeiadis, and the authors of "Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models", and the solutions are proposed by Jonas Oberhauser and Viktor Vafeiadis. Please refer to this link on the web: https://static.sched.com/hosted_files/osseu2022/e1/oss-eu22-jonas.pdf Signed-off-by: Jonas Oberhauser <jonas.oberhauser(a)huawei.com> Signed-off-by: Hanjun Guo <guohanjun(a)huawei.com> --- tools/memory-model/linux-kernel.bell | 9 ++-- tools/memory-model/linux-kernel.cat | 100 +++++++++++++++++++---------------- tools/memory-model/linux-kernel.def | 34 ++++++------ 3 files changed, 77 insertions(+), 66 deletions(-) diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index 5be86b1..880b28b 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -4,6 +4,8 @@ * Copyright (C) 2016 Luc Maranget <luc.maranget(a)inria.fr> for Inria * Copyright (C) 2017 Alan Stern <stern(a)rowland.harvard.edu>, * Andrea Parri <parri.andrea(a)gmail.com> + * Copyright (C) 2022 Jonas Oberhauser <jonas.oberhauser(a)huawei.com> + * Viktor Vafeiadis <viktor(a)mpi-sws.org> * * An earlier version of this file appeared in the companion webpage for * "Frightening small children and disconcerting grown-ups: Concurrency @@ -16,10 +18,11 @@ enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) || 'release (*smp_store_release*) || 'acquire (*smp_load_acquire*) || + 'seq-cst (*smp_load, xchg...*) || 'noreturn (* R of non-return RMW *) -instructions R[{'once,'acquire,'noreturn}] -instructions W[{'once,'release}] -instructions RMW[{'once,'acquire,'release}] +instructions R[{'seq-cst, 'once,'acquire,'noreturn}] +instructions W[{'seq-cst, 'once,'release}] +instructions RMW[{'seq-cst, 'once,'acquire,'release}] enum Barriers = 'wmb (*smp_wmb*) || 'rmb (*smp_rmb*) || diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index d70315f..9f14d31 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -4,6 +4,8 @@ * Copyright (C) 2016 Luc Maranget <luc.maranget(a)inria.fr> for Inria * Copyright (C) 2017 Alan Stern <stern(a)rowland.harvard.edu>, * Andrea Parri <parri.andrea(a)gmail.com> + * Copyright (C) 2022 Jonas Oberhauser <jonas.oberhauser(a)huawei.com>, + * Viktor Vafeiadis <viktor(a)mpi-sws.org> * * An earlier version of this file appeared in the companion webpage for * "Frightening small children and disconcerting grown-ups: Concurrency @@ -25,25 +27,33 @@ include "lock.cat" (*******************) (* Release Acquire *) + let acq-po = [Acquire] ; po ; [M] let po-rel = [M] ; po ; [Release] let po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po (* Fences *) -let R4rmb = R \ Noreturn (* Reads for which rmb works *) -let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb] -let wmb = [W] ; fencerel(Wmb) ; [W] -let mb = ([M] ; fencerel(Mb) ; [M]) | - ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | - ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | - ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | - ([M] ; po ; [UL] ; (co | po) ; [LKW] ; - fencerel(After-unlock-lock) ; [M]) -let gp = po ; [Sync-rcu | Sync-srcu] ; po? -let strong-fence = mb | gp - +let R4rmb = R \ Noreturn +let rmb = [R4rmb] ; po ; [Rmb] ; po ; [R4rmb] +let wmb = [W] ; po ; [Wmb] ; po ; [W] + +let rmb-plain = [R \ Noreturn] ; po ; [Rmb] ; po \ ( po ; [W] ; po-loc) ; [R \ Noreturn] +let plain-wmb = [W] ; po \ (po-loc ; [W] ; po) ; [Wmb] ; po ; [W] +let strong-fence = + [M] ; po ; [Mb] ; po ; [M] + | [M] ; po ; [Before-atomic] ; po ; [RMW] ; po? ; [M] + | [M] ; po? ; [RMW] ; po ; [After-atomic] ; po ; [M] + | [M] ; po? ; [LKW] ; po ; [After-spinlock] ; po ; [M] + | [M] ; po ; [UL] ; po ; [LKR] ; po ; [After-unlock-lock] ; po ; [M] + | [M] ; po? ; [SC] ; po ; [M] + | [M] ; po ; [SC] ; po? ; [M] + | po ; [Sync-rcu | Sync-srcu] ; po? +let strong-sync = strong-fence + | ([M] ; po-unlock-lock-po ; [After-unlock-lock] ; po ; [M]) let nonrw-fence = strong-fence | po-rel | acq-po let fence = nonrw-fence | wmb | rmb + + let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu | Before-atomic | After-atomic | Acquire | Release | Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) | @@ -64,35 +74,33 @@ empty rmw & (fre ; coe) as atomic (* Instruction execution ordering *) (**********************************) + (* Preserved Program Order *) -let dep = addr | data -let rwdep = (dep | ctrl) ; [W] -let overwrite = co | fr -let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) -let to-r = addr | (dep ; [Marked] ; rfi) -let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) +let dop = rmb-plain? ; (addr | data | ctrl | rfi)+; plain-wmb? +let to-w = (dop | po-loc) ; [W] +let lrs = ([W] ; po-loc ; [R]) \ (po-loc ; [W] ; po-loc) +let to-r = addr | ((addr | data) ; lrs) +let ppo = to-r | to-w | fence | (po ; [UL] ; po ; [LKR] ; po) (* Propagation: Ordering from release operations and strong fences. *) -let A-cumul(r) = (rfe ; [Marked])? ; r -let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb | - po-unlock-lock-po) ; [Marked] -let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; - [Marked] ; rfe? ; [Marked] +let cumul-fence = [Marked] ; (rfe? ; (po-rel ; (rfe ; rmw)*) | wmb | po-unlock-lock-po) ; [Marked] +let prop = [Marked] ; ((co | fr) & ext) ; cumul-fence* ; [Marked] ; rfe? ; [Marked] + (* * Happens Before: Ordering from the passage of time. - * No fences needed here for prop because relation confined to one process. *) -let hb = [Marked] ; (ppo | rfe | ((prop \ id) & int)) ; [Marked] -acyclic hb as happens-before +let hb = [Marked] ; (ppo | rfe | prop ; strong-sync) ; [Marked] +acyclic hb + +(* No fences needed here for prop because relation confined to one process. *) +irreflexive (prop ; ppo*) + + + + -(****************************************) -(* Write and fence propagation ordering *) -(****************************************) -(* Propagation: Each non-rf link needs a strong fence. *) -let pb = prop ; strong-fence ; hb* ; [Marked] -acyclic pb as propagation (*******) (* RCU *) @@ -118,7 +126,7 @@ let srcu-rscsi = srcu-rscs^-1 * one but two non-rf relations, but only in conjunction with an RCU * read-side critical section. *) -let rcu-link = po? ; hb* ; pb* ; prop ; po +let rcu-link = po? ; hb* ; prop? ; po (* * Any sequence containing at least as many grace periods as RCU read-side @@ -139,20 +147,20 @@ let rec rcu-order = rcu-gp | srcu-gp | ((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) | (rcu-order ; rcu-link ; rcu-order) let rcu-fence = po ; rcu-order ; po? -let fence = fence | rcu-fence -let strong-fence = strong-fence | rcu-fence +let fence-rcu = fence | rcu-fence +let strong-sync-rcu = strong-sync | rcu-fence -(* rb orders instructions just as pb does *) -let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked] +(* rb orders instructions just as hb does *) +let rb = prop? ; rcu-fence ; hb* ; [Marked] irreflexive rb as rcu (* - * The happens-before, propagation, and rcu constraints are all + * The happens-before and rcu constraints are all * expressions of temporal ordering. They could be replaced by * a single constraint on an "executes-before" relation, xb: * - * let xb = hb | pb | rb + * let xb = hb | rb * acyclic xb as executes-before *) @@ -166,24 +174,24 @@ let mixed-accesses = ([Plain & W] ; (po-loc \ barrier) ; [Marked]) | flag ~empty mixed-accesses as mixed-accesses (* Executes-before and visibility *) -let xbstar = (hb | pb | rb)* +let xbstar = (hb | rb)* let vis = cumul-fence* ; rfe? ; [Marked] ; - ((strong-fence ; [Marked] ; xbstar) | (xbstar & int)) + ((strong-sync-rcu ; [Marked] ; xbstar) | (xbstar & int)) (* Boundaries for lifetimes of plain accesses *) -let w-pre-bounded = [Marked] ; (addr | fence)? +let w-pre-bounded = [Marked] ; (addr | fence-rcu)? let r-pre-bounded = [Marked] ; (addr | nonrw-fence | ([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))? -let w-post-bounded = fence? ; [Marked] +let w-post-bounded = fence-rcu? ; [Marked] let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ; [Marked] (* Visibility and executes-before for plain accesses *) -let ww-vis = fence | (strong-fence ; xbstar ; w-pre-bounded) | +let ww-vis = (strong-sync-rcu ; xbstar ; w-pre-bounded) | (w-post-bounded ; vis ; w-pre-bounded) -let wr-vis = fence | (strong-fence ; xbstar ; r-pre-bounded) | +let wr-vis = (strong-sync-rcu ; xbstar ; r-pre-bounded) | (w-post-bounded ; vis ; r-pre-bounded) -let rw-xbstar = fence | (r-post-bounded ; xbstar ; w-pre-bounded) +let rw-xbstar = (r-post-bounded ; xbstar ; w-pre-bounded) (* Potential races *) let pre-race = ext & ((Plain * M) | ((M \ IW) * Plain)) diff --git a/tools/memory-model/linux-kernel.def b/tools/memory-model/linux-kernel.def index ef0f3c1..df239c2 100644 --- a/tools/memory-model/linux-kernel.def +++ b/tools/memory-model/linux-kernel.def @@ -14,7 +14,7 @@ smp_store_release(X,V) { __store{release}(*X,V); } smp_load_acquire(X) __load{acquire}(*X) rcu_assign_pointer(X,V) { __store{release}(X,V); } rcu_dereference(X) __load{once}(X) -smp_store_mb(X,V) { __store{once}(X,V); __fence{mb}; } +smp_store_mb(X,V) { __store{seq-cst}(X,V); } // Fences smp_mb() { __fence{mb}; } @@ -27,11 +27,11 @@ smp_mb__after_unlock_lock() { __fence{after-unlock-lock}; } barrier() { __fence{barrier}; } // Exchange -xchg(X,V) __xchg{mb}(X,V) +xchg(X,V) __xchg{seq-cst}(X,V) xchg_relaxed(X,V) __xchg{once}(X,V) xchg_release(X,V) __xchg{release}(X,V) xchg_acquire(X,V) __xchg{acquire}(X,V) -cmpxchg(X,V,W) __cmpxchg{mb}(X,V,W) +cmpxchg(X,V,W) __cmpxchg{seq-cst}(X,V,W) cmpxchg_relaxed(X,V,W) __cmpxchg{once}(X,V,W) cmpxchg_acquire(X,V,W) __cmpxchg{acquire}(X,V,W) cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W) @@ -65,52 +65,52 @@ atomic_sub(V,X) { __atomic_op(X,-,V); } atomic_inc(X) { __atomic_op(X,+,1); } atomic_dec(X) { __atomic_op(X,-,1); } -atomic_add_return(V,X) __atomic_op_return{mb}(X,+,V) +atomic_add_return(V,X) __atomic_op_return{seq-cst}(X,+,V) atomic_add_return_relaxed(V,X) __atomic_op_return{once}(X,+,V) atomic_add_return_acquire(V,X) __atomic_op_return{acquire}(X,+,V) atomic_add_return_release(V,X) __atomic_op_return{release}(X,+,V) -atomic_fetch_add(V,X) __atomic_fetch_op{mb}(X,+,V) +atomic_fetch_add(V,X) __atomic_fetch_op{seq-cst}(X,+,V) atomic_fetch_add_relaxed(V,X) __atomic_fetch_op{once}(X,+,V) atomic_fetch_add_acquire(V,X) __atomic_fetch_op{acquire}(X,+,V) atomic_fetch_add_release(V,X) __atomic_fetch_op{release}(X,+,V) -atomic_inc_return(X) __atomic_op_return{mb}(X,+,1) +atomic_inc_return(X) __atomic_op_return{seq-cst}(X,+,1) atomic_inc_return_relaxed(X) __atomic_op_return{once}(X,+,1) atomic_inc_return_acquire(X) __atomic_op_return{acquire}(X,+,1) atomic_inc_return_release(X) __atomic_op_return{release}(X,+,1) -atomic_fetch_inc(X) __atomic_fetch_op{mb}(X,+,1) +atomic_fetch_inc(X) __atomic_fetch_op{seq-cst}(X,+,1) atomic_fetch_inc_relaxed(X) __atomic_fetch_op{once}(X,+,1) atomic_fetch_inc_acquire(X) __atomic_fetch_op{acquire}(X,+,1) atomic_fetch_inc_release(X) __atomic_fetch_op{release}(X,+,1) -atomic_sub_return(V,X) __atomic_op_return{mb}(X,-,V) +atomic_sub_return(V,X) __atomic_op_return{seq-cst}(X,-,V) atomic_sub_return_relaxed(V,X) __atomic_op_return{once}(X,-,V) atomic_sub_return_acquire(V,X) __atomic_op_return{acquire}(X,-,V) atomic_sub_return_release(V,X) __atomic_op_return{release}(X,-,V) -atomic_fetch_sub(V,X) __atomic_fetch_op{mb}(X,-,V) +atomic_fetch_sub(V,X) __atomic_fetch_op{seq-cst}(X,-,V) atomic_fetch_sub_relaxed(V,X) __atomic_fetch_op{once}(X,-,V) atomic_fetch_sub_acquire(V,X) __atomic_fetch_op{acquire}(X,-,V) atomic_fetch_sub_release(V,X) __atomic_fetch_op{release}(X,-,V) -atomic_dec_return(X) __atomic_op_return{mb}(X,-,1) +atomic_dec_return(X) __atomic_op_return{seq-cst}(X,-,1) atomic_dec_return_relaxed(X) __atomic_op_return{once}(X,-,1) atomic_dec_return_acquire(X) __atomic_op_return{acquire}(X,-,1) atomic_dec_return_release(X) __atomic_op_return{release}(X,-,1) -atomic_fetch_dec(X) __atomic_fetch_op{mb}(X,-,1) +atomic_fetch_dec(X) __atomic_fetch_op{seq-cst}(X,-,1) atomic_fetch_dec_relaxed(X) __atomic_fetch_op{once}(X,-,1) atomic_fetch_dec_acquire(X) __atomic_fetch_op{acquire}(X,-,1) atomic_fetch_dec_release(X) __atomic_fetch_op{release}(X,-,1) -atomic_xchg(X,V) __xchg{mb}(X,V) +atomic_xchg(X,V) __xchg{seq-cst}(X,V) atomic_xchg_relaxed(X,V) __xchg{once}(X,V) atomic_xchg_release(X,V) __xchg{release}(X,V) atomic_xchg_acquire(X,V) __xchg{acquire}(X,V) -atomic_cmpxchg(X,V,W) __cmpxchg{mb}(X,V,W) +atomic_cmpxchg(X,V,W) __cmpxchg{seq-cst}(X,V,W) atomic_cmpxchg_relaxed(X,V,W) __cmpxchg{once}(X,V,W) atomic_cmpxchg_acquire(X,V,W) __cmpxchg{acquire}(X,V,W) atomic_cmpxchg_release(X,V,W) __cmpxchg{release}(X,V,W) -atomic_sub_and_test(V,X) __atomic_op_return{mb}(X,-,V) == 0 -atomic_dec_and_test(X) __atomic_op_return{mb}(X,-,1) == 0 -atomic_inc_and_test(X) __atomic_op_return{mb}(X,+,1) == 0 -atomic_add_negative(V,X) __atomic_op_return{mb}(X,+,V) < 0 +atomic_sub_and_test(V,X) __atomic_op_return{seq-cst}(X,-,V) == 0 +atomic_dec_and_test(X) __atomic_op_return{seq-cst}(X,-,1) == 0 +atomic_inc_and_test(X) __atomic_op_return{seq-cst}(X,+,1) == 0 +atomic_add_negative(V,X) __atomic_op_return{seq-cst}(X,+,V) < 0 -- 1.7.12.4

1 0

[PATCH for openEuler 22.09] Memory model: Fix the memory model issues for Linux kernel
by Hanjun Guo 24 Sep '22

24 Sep '22

From: Jonas Oberhauser <jonas.oberhauser(a)huawei.com> This the update and fixes for memory model, simplify the model by removing redundancies, making semantics of seq-cst explicit, making ppo a subset of po, making ppo locally computable, as well as eliminating several spurious bugs in qspinlock and litmus tests, and ensuring correct compilation to the official power model. These issues were detected by Jonas Oberhauser, Viktor Vafeiadis, and the authors of "Verifying and Optimizing Compact NUMA-Aware Locks on Weak Memory Models", and the solutions are proposed by Jonas Oberhauser and Viktor Vafeiadis. Signed-off-by: Jonas Oberhauser <jonas.oberhauser(a)huawei.com> Signed-off-by: Hanjun Guo <guohanjun(a)huawei.com> --- tools/memory-model/linux-kernel.bell | 9 ++-- tools/memory-model/linux-kernel.cat | 100 +++++++++++++++++++---------------- 2 files changed, 60 insertions(+), 49 deletions(-) diff --git a/tools/memory-model/linux-kernel.bell b/tools/memory-model/linux-kernel.bell index 5be86b1..880b28b 100644 --- a/tools/memory-model/linux-kernel.bell +++ b/tools/memory-model/linux-kernel.bell @@ -4,6 +4,8 @@ * Copyright (C) 2016 Luc Maranget <luc.maranget(a)inria.fr> for Inria * Copyright (C) 2017 Alan Stern <stern(a)rowland.harvard.edu>, * Andrea Parri <parri.andrea(a)gmail.com> + * Copyright (C) 2022 Jonas Oberhauser <jonas.oberhauser(a)huawei.com> + * Viktor Vafeiadis <viktor(a)mpi-sws.org> * * An earlier version of this file appeared in the companion webpage for * "Frightening small children and disconcerting grown-ups: Concurrency @@ -16,10 +18,11 @@ enum Accesses = 'once (*READ_ONCE,WRITE_ONCE*) || 'release (*smp_store_release*) || 'acquire (*smp_load_acquire*) || + 'seq-cst (*smp_load, xchg...*) || 'noreturn (* R of non-return RMW *) -instructions R[{'once,'acquire,'noreturn}] -instructions W[{'once,'release}] -instructions RMW[{'once,'acquire,'release}] +instructions R[{'seq-cst, 'once,'acquire,'noreturn}] +instructions W[{'seq-cst, 'once,'release}] +instructions RMW[{'seq-cst, 'once,'acquire,'release}] enum Barriers = 'wmb (*smp_wmb*) || 'rmb (*smp_rmb*) || diff --git a/tools/memory-model/linux-kernel.cat b/tools/memory-model/linux-kernel.cat index d70315f..9f14d31 100644 --- a/tools/memory-model/linux-kernel.cat +++ b/tools/memory-model/linux-kernel.cat @@ -4,6 +4,8 @@ * Copyright (C) 2016 Luc Maranget <luc.maranget(a)inria.fr> for Inria * Copyright (C) 2017 Alan Stern <stern(a)rowland.harvard.edu>, * Andrea Parri <parri.andrea(a)gmail.com> + * Copyright (C) 2022 Jonas Oberhauser <jonas.oberhauser(a)huawei.com>, + * Viktor Vafeiadis <viktor(a)mpi-sws.org> * * An earlier version of this file appeared in the companion webpage for * "Frightening small children and disconcerting grown-ups: Concurrency @@ -25,25 +27,33 @@ include "lock.cat" (*******************) (* Release Acquire *) + let acq-po = [Acquire] ; po ; [M] let po-rel = [M] ; po ; [Release] let po-unlock-lock-po = po ; [UL] ; (po|rf) ; [LKR] ; po (* Fences *) -let R4rmb = R \ Noreturn (* Reads for which rmb works *) -let rmb = [R4rmb] ; fencerel(Rmb) ; [R4rmb] -let wmb = [W] ; fencerel(Wmb) ; [W] -let mb = ([M] ; fencerel(Mb) ; [M]) | - ([M] ; fencerel(Before-atomic) ; [RMW] ; po? ; [M]) | - ([M] ; po? ; [RMW] ; fencerel(After-atomic) ; [M]) | - ([M] ; po? ; [LKW] ; fencerel(After-spinlock) ; [M]) | - ([M] ; po ; [UL] ; (co | po) ; [LKW] ; - fencerel(After-unlock-lock) ; [M]) -let gp = po ; [Sync-rcu | Sync-srcu] ; po? -let strong-fence = mb | gp - +let R4rmb = R \ Noreturn +let rmb = [R4rmb] ; po ; [Rmb] ; po ; [R4rmb] +let wmb = [W] ; po ; [Wmb] ; po ; [W] + +let rmb-plain = [R \ Noreturn] ; po ; [Rmb] ; po \ ( po ; [W] ; po-loc) ; [R \ Noreturn] +let plain-wmb = [W] ; po \ (po-loc ; [W] ; po) ; [Wmb] ; po ; [W] +let strong-fence = + [M] ; po ; [Mb] ; po ; [M] + | [M] ; po ; [Before-atomic] ; po ; [RMW] ; po? ; [M] + | [M] ; po? ; [RMW] ; po ; [After-atomic] ; po ; [M] + | [M] ; po? ; [LKW] ; po ; [After-spinlock] ; po ; [M] + | [M] ; po ; [UL] ; po ; [LKR] ; po ; [After-unlock-lock] ; po ; [M] + | [M] ; po? ; [SC] ; po ; [M] + | [M] ; po ; [SC] ; po? ; [M] + | po ; [Sync-rcu | Sync-srcu] ; po? +let strong-sync = strong-fence + | ([M] ; po-unlock-lock-po ; [After-unlock-lock] ; po ; [M]) let nonrw-fence = strong-fence | po-rel | acq-po let fence = nonrw-fence | wmb | rmb + + let barrier = fencerel(Barrier | Rmb | Wmb | Mb | Sync-rcu | Sync-srcu | Before-atomic | After-atomic | Acquire | Release | Rcu-lock | Rcu-unlock | Srcu-lock | Srcu-unlock) | @@ -64,35 +74,33 @@ empty rmw & (fre ; coe) as atomic (* Instruction execution ordering *) (**********************************) + (* Preserved Program Order *) -let dep = addr | data -let rwdep = (dep | ctrl) ; [W] -let overwrite = co | fr -let to-w = rwdep | (overwrite & int) | (addr ; [Plain] ; wmb) -let to-r = addr | (dep ; [Marked] ; rfi) -let ppo = to-r | to-w | fence | (po-unlock-lock-po & int) +let dop = rmb-plain? ; (addr | data | ctrl | rfi)+; plain-wmb? +let to-w = (dop | po-loc) ; [W] +let lrs = ([W] ; po-loc ; [R]) \ (po-loc ; [W] ; po-loc) +let to-r = addr | ((addr | data) ; lrs) +let ppo = to-r | to-w | fence | (po ; [UL] ; po ; [LKR] ; po) (* Propagation: Ordering from release operations and strong fences. *) -let A-cumul(r) = (rfe ; [Marked])? ; r -let cumul-fence = [Marked] ; (A-cumul(strong-fence | po-rel) | wmb | - po-unlock-lock-po) ; [Marked] -let prop = [Marked] ; (overwrite & ext)? ; cumul-fence* ; - [Marked] ; rfe? ; [Marked] +let cumul-fence = [Marked] ; (rfe? ; (po-rel ; (rfe ; rmw)*) | wmb | po-unlock-lock-po) ; [Marked] +let prop = [Marked] ; ((co | fr) & ext) ; cumul-fence* ; [Marked] ; rfe? ; [Marked] + (* * Happens Before: Ordering from the passage of time. - * No fences needed here for prop because relation confined to one process. *) -let hb = [Marked] ; (ppo | rfe | ((prop \ id) & int)) ; [Marked] -acyclic hb as happens-before +let hb = [Marked] ; (ppo | rfe | prop ; strong-sync) ; [Marked] +acyclic hb + +(* No fences needed here for prop because relation confined to one process. *) +irreflexive (prop ; ppo*) + + + + -(****************************************) -(* Write and fence propagation ordering *) -(****************************************) -(* Propagation: Each non-rf link needs a strong fence. *) -let pb = prop ; strong-fence ; hb* ; [Marked] -acyclic pb as propagation (*******) (* RCU *) @@ -118,7 +126,7 @@ let srcu-rscsi = srcu-rscs^-1 * one but two non-rf relations, but only in conjunction with an RCU * read-side critical section. *) -let rcu-link = po? ; hb* ; pb* ; prop ; po +let rcu-link = po? ; hb* ; prop? ; po (* * Any sequence containing at least as many grace periods as RCU read-side @@ -139,20 +147,20 @@ let rec rcu-order = rcu-gp | srcu-gp | ((srcu-rscsi ; rcu-link ; rcu-order ; rcu-link ; srcu-gp) & loc) | (rcu-order ; rcu-link ; rcu-order) let rcu-fence = po ; rcu-order ; po? -let fence = fence | rcu-fence -let strong-fence = strong-fence | rcu-fence +let fence-rcu = fence | rcu-fence +let strong-sync-rcu = strong-sync | rcu-fence -(* rb orders instructions just as pb does *) -let rb = prop ; rcu-fence ; hb* ; pb* ; [Marked] +(* rb orders instructions just as hb does *) +let rb = prop? ; rcu-fence ; hb* ; [Marked] irreflexive rb as rcu (* - * The happens-before, propagation, and rcu constraints are all + * The happens-before and rcu constraints are all * expressions of temporal ordering. They could be replaced by * a single constraint on an "executes-before" relation, xb: * - * let xb = hb | pb | rb + * let xb = hb | rb * acyclic xb as executes-before *) @@ -166,24 +174,24 @@ let mixed-accesses = ([Plain & W] ; (po-loc \ barrier) ; [Marked]) | flag ~empty mixed-accesses as mixed-accesses (* Executes-before and visibility *) -let xbstar = (hb | pb | rb)* +let xbstar = (hb | rb)* let vis = cumul-fence* ; rfe? ; [Marked] ; - ((strong-fence ; [Marked] ; xbstar) | (xbstar & int)) + ((strong-sync-rcu ; [Marked] ; xbstar) | (xbstar & int)) (* Boundaries for lifetimes of plain accesses *) -let w-pre-bounded = [Marked] ; (addr | fence)? +let w-pre-bounded = [Marked] ; (addr | fence-rcu)? let r-pre-bounded = [Marked] ; (addr | nonrw-fence | ([R4rmb] ; fencerel(Rmb) ; [~Noreturn]))? -let w-post-bounded = fence? ; [Marked] +let w-post-bounded = fence-rcu? ; [Marked] let r-post-bounded = (nonrw-fence | ([~Noreturn] ; fencerel(Rmb) ; [R4rmb]))? ; [Marked] (* Visibility and executes-before for plain accesses *) -let ww-vis = fence | (strong-fence ; xbstar ; w-pre-bounded) | +let ww-vis = (strong-sync-rcu ; xbstar ; w-pre-bounded) | (w-post-bounded ; vis ; w-pre-bounded) -let wr-vis = fence | (strong-fence ; xbstar ; r-pre-bounded) | +let wr-vis = (strong-sync-rcu ; xbstar ; r-pre-bounded) | (w-post-bounded ; vis ; r-pre-bounded) -let rw-xbstar = fence | (r-post-bounded ; xbstar ; w-pre-bounded) +let rw-xbstar = (r-post-bounded ; xbstar ; w-pre-bounded) (* Potential races *) let pre-race = ext & ((Plain * M) | ((M \ IW) * Plain)) -- 1.7.12.4

1 0

openEuler sig ai 例会
by openEuler conference 23 Sep '22

23 Sep '22

您好！ ai SIG 邀请您参加 2022-09-22 14:00 召开的Zoom会议会议主题：openEuler sig ai 例会会议链接：https://us06web.zoom.us/j/86057564964?pwd=UTltbmk4MFhZOFZwMnlyWlgrT3Y3QT09 会议纪要：https://etherpad.openeuler.org/p/ai-meetings 温馨提醒：建议接入会议后修改参会人的姓名，也可以使用您在gitee.com的ID 更多资讯尽在：https://openeuler.org/zh/ Hello! openEuler ai SIG invites you to attend the Zoom conference will be held at 2022-09-22 14:00, The subject of the conference is openEuler sig ai 例会, You can join the meeting at https://us06web.zoom.us/j/86057564964?pwd=UTltbmk4MFhZOFZwMnlyWlgrT3Y3QT09. Add topics at https://etherpad.openeuler.org/p/ai-meetings. Note: You are advised to change the participant name after joining the conference or use your ID at gitee.com. More information: https://openeuler.org/en/

2 1

sig-bidata例会
by openEuler conference 22 Sep '22

22 Sep '22

您好！ bigdata SIG 邀请您参加 2022-09-23 16:00 召开的Zoom会议会议主题：sig-bidata例会会议链接：https://us06web.zoom.us/j/85865044706?pwd=Y2svbXR4TXdueTJzVERkR044Rkd5dz09 会议纪要：https://etherpad.openeuler.org/p/bigdata-meetings 温馨提醒：建议接入会议后修改参会人的姓名，也可以使用您在gitee.com的ID 更多资讯尽在：https://openeuler.org/zh/ Hello! openEuler bigdata SIG invites you to attend the Zoom conference will be held at 2022-09-23 16:00, The subject of the conference is sig-bidata例会, You can join the meeting at https://us06web.zoom.us/j/85865044706?pwd=Y2svbXR4TXdueTJzVERkR044Rkd5dz09. Add topics at https://etherpad.openeuler.org/p/bigdata-meetings. Note: You are advised to change the participant name after joining the conference or use your ID at gitee.com. More information: https://openeuler.org/en/

1 0

TC委员变更评审，请各位委员邮件回复发表意见
by Huxinwei 19 Sep '22

19 Sep '22

@各位技术委员会委员：彭成寒因为个人工作原因，无法继续在技术委员会中服务，申请退出。成寒推荐赵川峰接任，附件是川峰在本周三TC例会上的个人介绍申请，请各位技术委员会委员审视后邮件反馈意见。谢谢 Regards Xinwei

16 16

TC双周例会
by openEuler conference 19 Sep '22

19 Sep '22

您好！ TC SIG 邀请您参加 2022-09-21 10:00 召开的Zoom会议(自动录制) 会议主题：TC双周例会会议内容：技术委员会双周例会会议链接：https://us06web.zoom.us/j/85345756009?pwd=ditMdExTcWQrRWRzUGVrSG9MTURFZz09 会议纪要：https://etherpad.openeuler.org/p/TC-meetings 温馨提醒：建议接入会议后修改参会人的姓名，也可以使用您在gitee.com的ID 更多资讯尽在：https://openeuler.org/zh/ Hello! openEuler TC SIG invites you to attend the Zoom conference(auto recording) will be held at 2022-09-21 10:00, The subject of the conference is TC双周例会, Summary: 技术委员会双周例会 You can join the meeting at https://us06web.zoom.us/j/85345756009?pwd=ditMdExTcWQrRWRzUGVrSG9MTURFZz09. Add topics at https://etherpad.openeuler.org/p/TC-meetings. Note: You are advised to change the participant name after joining the conference or use your ID at gitee.com. More information: https://openeuler.org/en/

2 1

TC例会议题申请
by 郑振宇 19 Sep '22

19 Sep '22

申请议题：openEuler社区开发者贡献看板开发进展及上线计划内容简介：为进一步实现社区透明治理，openEuler社区开发者贡献看板新增SIG组贡献详情、个人开发者贡献详情、社区企业贡献详情等相关维度的贡献统计，并计划近期上线；本次议题为TC介绍看板整体开发进展、权限设置以及上线策略，并收集意见反馈。感谢

1 0

[新SIG提案]申请新建SIG组sig-ebpf-practice
by 17323181547 15 Sep '22

15 Sep '22

2 1

2024

2023

2022

2021

2020

2019

Tc