EagleBear2002 的博客

$$ \def\put{\mathrm{put}} \def\get{\mathrm{get}} \def\rem{\mathrm{rem}} \def\inv \def\ret \def\hb \def\lin $$

摘要

多线程程序通常依赖高效且线程安全的并发对象，如集合、键值映射和队列。虽然一些并发对象的操作被设计为原子性行为，见证其在线性化顺序中的前驱操作的原子效果，但其他操作为了避开复杂的控制和同步瓶颈而放弃了这种强一致性。例如，键值映射的 contains(value) 方法可能在不阻塞并发更新的情况下遍历键值条目，以避免不必要的性能瓶颈，因此可能会忽略某些在线性化顺序上的前驱操作的效果。尽管这些弱一致性的操作可能不具备原子性，但它们仍然提供了一些保证，比如只观察到已经存在的值。

在这项工作中，我们开发了一种方法来证明并发对象实现遵循弱一致性规范。特别是，我们考虑了对放宽可见性规范的（前向）模拟证明，允许指定的操作忽略它们的一些线性化顺序上的前驱操作，即表现得好像这些操作从未发生过一样。除了标注实现代码以识别逻辑效应发生的点（即操作的线性化点），我们还标注代码以识别可见操作，即那些效果被观察到的操作；实际上，这种标注可以通过跟踪每个访问内存位置的写入者自动完成。我们在一个通用的状态转换系统概念上形式化了我们的方法论，该概念独立于任何特定的编程语言或内存模型，并展示了其应用。

Introduction

$$ \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\soo{\mathsf{\textcolor{purple}{soo}}} \def\wr{\mathsf{\textcolor{teal}{wr}}} \def\ww{\mathsf{\textcolor{red}{ww}}} \def\rw{\mathsf{\textcolor{blue}{rw}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\WR{\mathsf{\textcolor{teal}{WR}}} \def\CM{\mathsf{\textcolor{orange}{CM}}} \def\CO{\mathsf{\textcolor{brown}{CO}}} \def\AR{\mathsf{\textcolor{pink}{AR}}} \def\vis{\mathsf{\textcolor{orange}{vis}}} \def\VIS{\mathsf{\textcolor{orange}{VIS}}} \def\hb{\mathsf{\textcolor{pink}{hb}}} \def\hbo{\mathsf{\textcolor{pink}{hbo}}} \def\A{\mathsf{A}} \def\E{\mathsf{E}} \def\cc{\mathsf{cc}} \def\ec{\mathsf{ec}} \def\sc{\mathsf{sc}} \def\rc{\mathsf{rc}} \def\mav{\mathsf{mav}} \def\rr{\mathsf{rr}} \def\sameobj{\mathsf{sameobj}} \def\oper{\mathsf{oper}} \def\txn{\mathsf{txn}} \def\sametxn{\mathsf{sametxn}} \def\withdraw{\mathtt{withdraw}} \def\deposit{\mathtt{deposit}} \def\getBalance{\mathtt{getBalance}} \def\heta{\hat{\eta}} \def\RYW{\mathbf{RYW}} \def\MR{\mathbf{MR}} \def\MW{\mathbf{MW}} \def\WFR{\mathbf{WFR}} $$

摘要

面向用户的在线服务采用地理分布的数据存储来减少延迟并容忍部分故障，以提供快速且始终可用的体验。然而，地理分布并非没有代价；应用程序开发者需要处理弱一致性行为，并且缺乏构建高级复制数据类型的抽象机制，这导致了复杂的应用程序逻辑，并不可避免地将不一致性暴露给用户。一些商业分布式数据存储和多个学术提案提供了一致性级别的层次结构，更强的一致性保证会带来更高的延迟和吞吐量成本。然而，正确为操作分配合适的一致性级别需要细致的推理，并且通常是一个容易出错的任务。

在本文中，我们提出了 QUELEA，一种针对最终一致性的数据存储（ECDS）的声明式编程模型，它配备了一种契约语言，能够指定细粒度的应用层一致性属性。一个契约执行系统分析这些契约，并自动生成受保护方法所需的一致性协议。我们在一个现成的支持无协调事务的 ECDS 之上实现了 QUELEA。通过包括两个大型网络应用在内的几个基准测试，展示了我们的方法的有效性。

关键词：最终一致性、可用性、CRDT、公理合约、合约分类、分布式事务、SMT 求解器、可判定逻辑、Quelea、Cassandra、Haskell

$$ \def\po{\mathsf{\textcolor{red}{po}}} \def\so{\mathsf{\textcolor{purple}{so}}} \def\hbs{\mathsf{hbs}} \def\wr{\mathsf{\textcolor{teal}{wr}}} \def\ww{\mathsf{\textcolor{red}{ww}}} \def\rw{\mathsf{\textcolor{blue}{rw}}} \def\co{\mathsf{\textcolor{orange}{co}}} \def\SO{\mathsf{\textcolor{purple}{SO}}} \def\WR{\mathsf{\textcolor{teal}{WR}}} \def\CM{\mathsf{\textcolor{orange}{CM}}} \def\CO{\mathsf{\textcolor{brown}{CO}}} $$

摘要

有效的软件规格说明能够支持模块化推理，允许客户端在不了解模块实现细节的情况下建立程序属性。虽然一些模块的操作表现得像原子操作一样，但其他模块为了提高性能而采用了较弱的一致性。由于当前的方法无法捕捉到具有不同非原子一致性水平的操作所提供的保证，因此规格说明变得无效，失去了为调用非原子操作的程序建立属性的能力。

在这项工作中，我们开发了一种方法来指定那些操作满足多个不同一致性级别的软件模块。特别是，我们开发了一个简单的注释语言，通过可见性放松来指定弱一致性操作，在这种注释中对操作之间的可见性施加了不同的约束。为了与现代软件平台集成，我们识别了一种新的称为“顺序发生前一致性”的一致性特性，它允许有效验证。实验上，我们通过推导和验证 Java 并发对象的放松可见性规格说明，展示了我们方法的有效性。此外，我们还通过实验证明了我们的注释语言是优化的，即使更细粒度的语言也不能为 Java 对象提供更强的规格说明。

作者：

摘要

本文记录了南京大学师生免费领取华为云云主机的步骤，以供参考。

领取步骤

1. 手机下载“华为云 APP”并注册、登录；
2. 使用“华为云 APP”扫描文档中的二维码（本文不提供二维码）；
3. 自动跳转云主机领取配置页面（这一步骤需要时间，请耐心等待）；

摘要

商业数据库支持不同的隔离级别，以允许程序员在一致性和性能提升之间做出权衡。隔离级别在当前的 ANSI 标准中定义，但定义含糊不清，而为纠正该问题而提出的修订定义过于受限，因为它们仅允许悲观（锁定）实现。本文介绍了 ANSI 级别的新规范。我们的规范是可移植的；它们不仅适用于锁定实现，还适用于乐观和多版本并发控制方案。此外，与早期的定义不同，我们的新规范在所有级别上以正确且灵活的方式处理谓词。

Introduction

本文给出了 ANSI-SQL 隔离级别的新、精确定义 [6]。与以前的提案 [13、6、8] 不同，新定义既正确（它们排除了所有不良历史记录），又独立于实现。我们的规范允许使用各种并发控制技术，包括锁定、乐观技术 [20、2、5] 和多版本机制 [9、24]。因此，它们符合 ANSI-SQL 的目标，可以用作隔离标准。

隔离级别的概念最初是在 [13] 中以一致性程度的名称引入的。这项工作的目标是通过牺牲完全隔离的保证来为工作负载提供更好的并发性。[13] 中的工作和 [11] 建议的一些改进为 ANSI/ISO SQL-92 隔离级别定义 [6] 奠定了基础，其目标是制定一个独立于实现的标准。然而，后续论文 [8] 表明 [6] 中提供的定义含糊不清。该论文提出了避免歧义问题的不同定义，但如 [8] 所述，这些定义只是“锁定的伪装版本”，因此不允许乐观和多版本机制。因此，这些定义未能满足 ANSI-SQL 关于实现独立性的目标。

摘要

数据异常尚没有统一的定义, 其含义是指可能破坏数据库一致性状态的特定数据操作模式. 已知的数据异常有脏写、脏读、不可重复读、幻读、丢失更新、读偏序和写偏序等. 为了提高并发控制算法的效率, 数据异常也被用于定义隔离级别, 采用较弱的隔离级别以提高事务处理系统的效率. 体系化地研究了数据异常以及对应的隔离级别, 发现了 22 种未被其他文献报告过的新的数据异常, 并对全部数据异常进行分类. 基于数据异常的分类, 提出了新的且不同粒度的隔离级别体系, 揭示基于数据异常定义隔离级别的规律, 使得对于数据异常和隔离级别等相关概念的认知可以更加简明.

摘要

SQL Isolation Levels

上一节讨论了手动控制每个应用程序甚至每个事务的锁定持续时间的想法，通过仅允许应用程序架构师或开发人员选择有限数量的“锁定样式”选项，可以使其更加安全。这些选项称为隔离级别，其中之一就是通常的冲突可串行化概念，它们甚至已被纳入 SQL 标准。通过发出相应的 SQL 命令“set isolation level …”来选择特定的隔离级别

SQL 标准支持的隔离级别是根据与（强）严格两阶段锁定的受控偏差来定义的。然而，它们应该被理解为调度类，尽管是由特定的锁定协议生成的，但可以通过服务器选择使用的任何适当的并发控制算法来强制执行。实际上最重要的隔离级别定义如下：

定义 10.1 隔离级别

如果根据 S2PL 获取和释放写锁，即所有写锁都保持到事务结束，则称调度 s 在隔离级别读未提交（Read Uncomitted，也称为脏读或浏览级别）下运行。

如果根据 S2PL 获取和释放写锁，并且读锁（至少）在客户端发出的每个数据服务器操作的持续时间内保持，则称调度 s 在隔离级别读已提交（Read Comitted，也称为游标稳定性级别）下运行。

如果调度 s 可以通过 S2PL 协议生成，则称调度 s 在隔离级别（冲突）可串行化（SER）下运行。

摘要

本文是视频 https://www.bilibili.com/video/BV1RN41157MW/?spm_id_from=333.1007.top_right_bar_window_history.content.click&vd_source=bd427f91dee5122f5f148ab719220125 的文本提取。

这是大连的海浪声，这是黄河的雷鸣，这是长江的悠叹。它们已经在这片土地上回响了数万年，贯穿我们的历史。

江河湖海，这是中国人对自然水体的称谓，人总是在以各种各样的方式征服和改造自然，而从古至今我们征服水体的方式从没有变过——造船。

一叶舟

摘要

全球造船业经历了深刻的变革，其范围、复杂性和贸易影响都呈现出多样化。本研究通过分析日本、韩国和中国造船企业的演变模式来探讨这些转变。我们踏上一段历史之旅，追溯行业领导地位从欧洲向亚洲的转变。作为案例研究，我们详细研究了韩国造船业从国内优势到全球地位的五个转型阶段。为了建立一个涵盖日本、韩国和中国造船业的比较框架，我们引入了两个关键参数：创新价值交付能力和全球市场定位。这些参数阐明了这三个亚洲国家在造船领域采取的独特发展路径。我们的研究结果强调，在竞争加剧和地缘政治动态不断变化的环境中，领先的公司战略性地利用其国家制造优势和物流基础设施，同时巧妙地应对全球政治的复杂性和各自国家所奉行的产业政策。这项研究为未来对后疫情时代全球船舶制造业的研究提供了宝贵的见解和启示。

关键词：Shipbuilding industry · Comparative studies · Competitive landscape · Growth theory · Japan · Korea · China

Introduction

全球造船业曾经以西方为中心，近几十年来踏上了变革之旅。尖端技术的出现和贸易动态的演变推动了深刻的转变，重塑了竞争格局。目前，该行业的中心位于亚太地区，日本、韩国和中国处于领先地位（Yum 2022；Gavalas 等 2022）。这些国家在造船业的崛起与其制造业的增长同步，包括钢铁、化学品、汽车、电子和半导体（Jiang 等 2013；Oh 和 Rhee 2008；Park 等 2022；Park 和 Jeong 2012）。尽管有值得注意的研究贡献侧重于过去二十年的变化（Bruno 和 Tenold 2011；Shin 和 Hassink 2011；Ferreira 等人 2018），但我们对包括 2000-2020 年代在内的亚洲造船业全面转型的理解仍然严重不足（Feng 等人 2023b；Gavalas 等人 2022；Park 等人 2021）。鉴于全球格局瞬息万变，竞争加剧，地缘政治动态不断演变，这一差距尤为紧迫。

摘要

经典哲学的危机揭示了人们对提供数学基础的数学和哲学标准的困惑。

题目中提到的三个学派都试图给数学提供一个坚实的基础，三个危机意味着这些学派未能完成其任务。本文“以现代的眼光”审视这些危机，使用今天可用的数学，而不仅仅是创建这些学派的先驱们所用的数学。因此，本文不以严格的历史方式来处理这三个危机，也不讨论目前大量的、技术性的数学，这些数学是由上述三个学派所引入的技术而产生的。原因之一是，这样的讨论需要一本书，而不是一篇短文；原因之二是，所有这些技术性数学与数学哲学关系不大，而在这篇文章中，我想强调逻辑主义、直觉主义和形式主义中那些建立在哲学之上的内容。

本文转载自柳渝科学网博客：科学网—数学中的三个危机 ：逻辑主义、直觉主义和形式主义 - 译文（1）：逻辑主义 - 柳渝的博文

逻辑主义