- Tc - mailweb.openeuler.org

17 Oct '22

尊敬的技术委员会: 为提高网络高可用性，我司申请新SIG“sig-high-availability-network”，计划在欧拉社区开源PRIP软件。 PRIP（Parallel Redundancy Internet Protocol）并行冗余互联协议，是由北京凝思软件股份有限公司提出并制定的适用于冗余网络通信协议，PRIP并行冗余互联协议可完全满足冗余通信的基本功能要求和0延时切换的性能要求，并且完全基于软件实现。 PR链接：https://gitee.com/openeuler/community/pulls/4161 工作目标：网络高可用软件致力于打造高性能、高可靠性、故障0延迟切换的目标。为企业提供坚实稳定的网络环境,同时更好的支撑和扩展上层业务应用。软件本身要不断的进行优化迭代,以适用多种网络拓扑环境。网络高可用软件将适配支持主流开源Linux操作系统,并提高友好的软件安装方式。同时将源码开源Linux内核社区,并根据Linux内核longterm的版本进行长期维护更新。 - 基于软件实现,不依赖特殊的网络设备和网络拓扑 - 单链路故障的情况下,用户数据通信数据无影响 - 对操作系统正常的网络功能不产生干扰和影响 - 对用户程序透明 - 提供软件代码仓库与发行版,提供给欧拉社区和外部用户 - 深耕网络高可用技术,研究先进的使用场景,提供软件解决方案工作计划： 1. 完成对openEuler 20.03(内核版本4.19)系统的适配; 2022年10月17日～2022年11月6日 2. 在openEuler 20.03系统进行测试，并提交社区; 2022年11月7日～2022年11月13日 3. 完成对openEuler 22.03(内核版本5.10)系统的适配; 2022年11月14日～2022年12月4日 4. 在openEuler 20.03系统进行测试，并提交社区; 2022年12月5日～2022年12月10日 5. 对社区反馈的PRIP软件使用和功能相关的问题提供支持长期申请人：北京凝思软件 -- Thanks and Regards ======================================================= 高泽(成都研发1部) 北京凝思软件股份有限公司四川分公司研发部手机：18993436360 网址：www.linx-info.com 地址：成都市高新区天府大道中段530号东方希望天祥广场B座3401 邮编：610000

2 1

dev-util SIG例会
by openEuler conference 17 Oct '22

17 Oct '22

您好！ dev-utils SIG 邀请您参加 2022-10-17 16:00 召开的Zoom会议会议主题：dev-util SIG例会会议内容： sysmaster（gitee.com/openeuler/sysmaster）项目使用Rust重新思考和实现1号进程。会议链接：https://us06web.zoom.us/j/84908413285?pwd=NkNIK2tCWWpOdndqYnBVSnBJckowdz09 会议纪要：https://etherpad.openeuler.org/p/dev-utils-meetings 温馨提醒：建议接入会议后修改参会人的姓名，也可以使用您在gitee.com的ID 更多资讯尽在：https://openeuler.org/zh/ Hello! openEuler dev-utils SIG invites you to attend the Zoom conference will be held at 2022-10-17 16:00, The subject of the conference is dev-util SIG例会, Summary: sysmaster（gitee.com/openeuler/sysmaster）项目使用Rust重新思考和实现1号进程。 You can join the meeting at https://us06web.zoom.us/j/84908413285?pwd=NkNIK2tCWWpOdndqYnBVSnBJckowdz09. Add topics at https://etherpad.openeuler.org/p/dev-utils-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

会议纪要：安全委员会&安全技术sig例会 2022-10-12
by Weigang (Jimmy) 12 Oct '22

12 Oct '22

2022-10-12 16:00~17:30 会议主题：安全委员会&安全技术sig例会主持人：魏刚与会人：华为-魏刚、天翼云-游益锋，天翼云-吴开顺，天翼云-曾昊，天翼云-刘工，麒麟软件-崔雷，统信-魏东，华为-颜小兵，suse-毛晨曦，华为-朱健伟，中科微澜-闫志全，麒麟软件-杨昭，xu 会议议题： 1、社区漏洞感知情况汇报 - 闫志全 • 9/8至今提交漏洞240余条，全部满足感知24小时的时效要求，误报11条，误报率4.6%。 2、社区漏洞修复情况汇报 - 颜小兵 • 9月份发布了安全公告 105个，公告修复的漏洞256个，公告不受影响的漏洞396个。 3、关于suse加入受限披露邮件列表的申请评审 - 魏刚 • 安全委员会全员通过。欢迎suse加入受限披露邮件列表（即发行商列表）。 4、收集OSV对于社区CVE推送和通知处理流程的需求 - 魏刚 • 收集内容：收集各个具体业务场景中CVE处理流程上的不足 • 收集方式：安全委员会代码仓issue vs 白板？创建issue，纪要发送。 • **请各OSV及用户将您的反馈意见在10/23前以评论的形式反馈到以下链接所代表的issue中** • https://gitee.com/openeuler/security-committee/issues/I5VE2C 5、讨论安全委员会运作规范- 魏刚 • 重新讨论了9月跟TC初步汇报过的内容，暂时没有进一步的修改建议。 • 遗留问题：将新的运作规范内容合入安全委员会gitee仓的已有文档，提交PR供大家评审。-- 魏刚，下次例会前 6、其它： • 麒麟软件杨昭代表rancher sig反馈希望社区基础设施提供容器镜像CVE扫描能力。已将此需求合入上述OSV需求收集结果。下次会议时间10.26, 主持人：谈静国

1 0

会议纪要：安全委员会&安全技术sig例会 2022-10-12
by Weigang (Jimmy) 12 Oct '22

12 Oct '22

2022-10-12 16:00~17:30 会议主题：安全委员会&安全技术sig例会主持人：魏刚与会人：华为-魏刚、天翼云-游益锋，天翼云-吴开顺，天翼云-曾昊，天翼云-刘工，麒麟软件-崔雷，统信-魏东，华为-颜小兵，suse-毛晨曦，华为-朱健伟，中科微澜-闫志全，麒麟软件-杨昭，xu 会议议题： 1、社区漏洞感知情况汇报 - 闫志全 • 9/8至今提交漏洞240余条，全部满足感知24小时的时效要求，误报11条，误报率4.6%。 2、社区漏洞修复情况汇报 - 颜小兵 • 9月份发布了安全公告 105个，公告修复的漏洞256个，公告不受影响的漏洞396个。 3、关于suse加入受限披露邮件列表的申请评审 - 魏刚 • 安全委员会全员通过。欢迎suse加入受限披露邮件列表（即发行商列表）。 4、收集OSV对于社区CVE推送和通知处理流程的需求 - 魏刚 • 收集内容：收集各个具体业务场景中CVE处理流程上的不足 • 收集方式：安全委员会代码仓issue vs 白板？创建issue，纪要发送。 • **请各OSV及用户将您的反馈意见在10/23前以评论的形式反馈到以下链接所代表的issue中** • https://gitee.com/openeuler/security-committee/issues/I5VE2C 5、讨论安全委员会运作规范- 魏刚 • 重新讨论了9月跟TC初步汇报过的内容，暂时没有进一步的修改建议。 • 遗留问题：将新的运作规范内容合入安全委员会gitee仓的已有文档，提交PR供大家评审。-- 魏刚，下次例会前 6、其它： • 麒麟软件杨昭代表rancher sig反馈希望社区基础设施提供容器镜像CVE扫描能力。已将此需求合入上述OSV需求收集结果。下次会议时间10.26, 主持人：谈静国

1 0

sig bigdata例会
by openEuler conference 12 Oct '22

12 Oct '22

您好！ bigdata SIG 邀请您参加 2022-10-14 16:00 召开的Zoom会议(自动录制) 会议主题：sig bigdata例会会议内容： sig bigdata例会，欢迎申报议题！会议链接：https://us06web.zoom.us/j/85374519378?pwd=c3VBTzhHOTNxVzZrY3JTNmFZMXQ5QT09 会议纪要：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(auto recording) will be held at 2022-10-14 16:00, The subject of the conference is sig bigdata例会, Summary: sig bigdata例会，欢迎申报议题！ You can join the meeting at https://us06web.zoom.us/j/85374519378?pwd=c3VBTzhHOTNxVzZrY3JTNmFZMXQ5QT09. 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

sig-DPU双周例会
by openEuler conference 11 Oct '22

11 Oct '22

您好！ sig-DPU SIG 邀请您参加 2022-10-13 10:00 召开的Zoom会议(自动录制) 会议主题：sig-DPU双周例会会议链接：https://us06web.zoom.us/j/84159897085?pwd=TUY4UytVNUJtdTU5RjJuaWx3bnQzQT09 会议纪要：https://etherpad.openeuler.org/p/sig-DPU-meetings 温馨提醒：建议接入会议后修改参会人的姓名，也可以使用您在gitee.com的ID 更多资讯尽在：https://openeuler.org/zh/ Hello! openEuler sig-DPU SIG invites you to attend the Zoom conference(auto recording) will be held at 2022-10-13 10:00, The subject of the conference is sig-DPU双周例会, You can join the meeting at https://us06web.zoom.us/j/84159897085?pwd=TUY4UytVNUJtdTU5RjJuaWx3bnQzQT09. Add topics at https://etherpad.openeuler.org/p/sig-DPU-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 openEuler conference 11 Oct '22

11 Oct '22

您好！ 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/

4 3

答复: [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