在SPIN/Promela中模拟CAS(Compare-and-Swap)

CAS(Compare-And-Swap)是一种在多线程编程中常用的数据同步方法,它通过比较和交换操作来保证数据的一致性。然而,在SPIN/Promela中没有直接的CAS对应实现。

让我们来看 …

more ...


A2B Game Solutions

A2B is a "zach-like" programming game, which let you to use a very simple "programming language" to solve different problems for strings.

Personally, I highly recommand this game along with "Shenzhen IO" and "Factorio" as an beginner tutorial for anyone who wants to be a software engineer.

Spoiler Alert

** The …

more ...

浅淡TCP BBR

背景

在一对跨地域的机器(美国<->香港),使用TCP(Cubic拥塞控制算法)通信throughput最高2MB/s,丢包率0.02%。使用UDP通信throughput最高能达到140MB/s。

这是一个非常典型的长肥管道(LFN),并且丢包 …

more ...

论文阅读-WiscKey:SSD友好的KV分离存储引擎

背景

基于LSM-Tree的存储引擎

Log-Structed Merge-Tree (a.k.a. LSM-Tree)是当下常用的一种基于磁盘的存储引擎。与Hash索引和B-Tree同为数据库核心的数据结构。

LSM-Tree的优势在于:

  1. 无需将所有的Key索引在内存中。可以通过分级查找的方式,查 …
more ...

我到底从UW-CSE341学到了什么

TL;DR 什么也没学到

课程首页

Coursera-课程-A, B, C

介绍当中说,本课程主要内容是FP,并且顺道讨论一下程序语言的设计。

UW官方上面的课程只有Slides和assignments,video不提供。Coursera有video,但是 …

more ...

Introduction to Ceph

什么是Ceph

Ceph是一个可扩展的,高性能的分布式存储系统。提供了三种不同类型的接口以适应不同的应用场景:

  • block-based: 块存储,可以用做VM的虚拟磁盘
  • object-based: 对象 …
more ...



白话一致性协议 - Paxos、Raft和PacificA[2]

PacificA是一个框架

虽然在题目中我们把Paxos、Raft和PacificA并列,但是Paxos和Raft在论文中称自己为一种“算法”(algorithm);而PacificA对自己的定位是一种通用的,强一致的数据同步框架

在论文中,作者提到现有的可证明的数据同步协 …

more ...