3.数学视角的操作系统

Python 建模操作系统

在理解了 “软件 (应用)” 和 “硬件 (计算机)” 之后，操作系统就是直接运行在计算机硬件上的程序，它提供了应用程序执行的支撑和一组 API (系统调用)：操作系统内核被加载后，拥有完整计算机的控制权限，包括中断和 I/O 设备，因此可以构造出多个应用程序同时执行的 “假象”。

• 应用程序来看，操作系统就是一条 syscall 指令

• 硬件来看，操作系统就是一个 C 程序，我们能从cpureset开始运行状态机，加载自己的代码，操作系统iu能运行起来

当我们一直说程序是状态机的时候，我们有没有可能，把这个状态机画出来。

1. 程序正确性的证明

程序的本质

数学视角的程序。首先数学是严格的，但数学的“严格性”是有人类保证的，一个问题，数学史人类发明的还是有人类发现的。

程序是一种“数学严格”的对象。

• 程序 = 初始状态 + 迁移函数

• 此视角下，程序和数学对象无限接近

程序是一个函数 $f(\cdot)$ 机器角度，一串0和1，这串数学就代表了下一个状态。

觉得编程很困难，是因为人类并不擅长数学严格，常常写出似是而非的代码。袋盖是正确的，但是总是被编译器提醒有错。比如 for (int j=0; j<n; i++) 两层循环里，人会犯的错误。

程序是被逼无奈的，为了使用这个机器，只好去写数学严格的程序，人需要去写程序。

程序是人类的，但也是反人类的，。

• 程序连接了人的需求，是给人看的

• 程序会在机器上执行，编程的错误来源于人对程序的行为没有 100% 的掌握

---

当谈程序是个数学对象的时候，即程序是个数学意义上的函数，主要是想研究程序的正确性。

如何证明程序正确性

2. 为操作系统建模

3. 数学视角的操作系统

操作系统的状态机模型

gdb，每一步都能看到状态，然后往前走一步。

存在的问题是，状态太多了。当我们想去看初始状态，都要去查很厚的手册。

所以理论上做理解没有任何问题，实际也是这样的。但是真的要画状态机，并不容易。

所以需要简化。

• 操作系统里有这种工具，strace，把状态简化成操作系统和应用软件的边界。

把汇编状态机简化成C的状态机，C是高级汇编，我们可以用更高级的语言模拟实现这个行为。

我们只关心纯粹的计算和系统调用。

建模，玩具操作系统

四个 “系统调用” API

• choose(xs): 返回 xs 中的一个随机选项

• write(s): 输出字符串 s

• spawn(fn): 创建一个可运行的状态机 fn

• sched(): 随机切换到任意状态机执行

比如 choose(['Head','Tail']) 随即返回一个。如果只做纯粹的计算，想在两个里面随便选一个，必须借助外界帮忙。

除此之外，所有的代码都是确定 (deterministic) 的纯粹计算

比如

def main():
    sys_write('Hello, OS World\n')  # sys_write -> print

def main()
    x = sys_choose(['Head','Tail'])
    x = x.lower()
    sys_write(f'{x}\n')

使用操作系统api然后做纯粹的计算，然后再做调用。write在程序看来，没有任何可观测的效果，程序这个状态机没有发生变化。

但是如果从操作系统的角度来看，操作系统是个更大的状态机。操作系统的状态在这个时候发生变化，比如 stdout 里的 buffer 在写入了东西。还个角度，程序执行的时候，操作系统自己这个状态机是不是就是不变得。

这个角度来思考，操作系统就是这些状态的管理者。

管理状态机最重要的api就是 spawn。它的行为是原来的状态机往前挪一步(pc+1)，然后创建一个新的状态机。

现在有了新的问题，有了两个状态机，那么下一步该执行哪一个呢？

操作系统

这个玩具的好处是把完整的状态机画出来，这要比画C的状态机简单的多。

count = 0

def Tprint(name):
    global count
    for i in range(3):
        count += 1
        sys_write(f'#{count:02} Hello from {name}{i+1}\n')
        sys_sched()

def main():
    n = sys_choose([3, 4, 5])
    sys_write(f'#Thread = {n}\n')
    for name in 'ABCDE'[:n]:
        sys_spawn(Tprint, name)
    sys_sched()

选用 python，那么如何实现这些模拟的系统调用呢？

有些实现是显而易见的，比较麻烦的是任务切换时如何对状态机封存使得在切换回来时能继续执行状态机。

真实的操作系统，除了程序主动用系统调用交出控制权，也会被动的交出，用时钟中断保证每个程序都可以被打断。

操作系统，在初始的时候有个 main 函数，随便选一个任务执行，然后根据任务的返回，确定下一步的操作。

这些操作可以模拟出一些很有意思的行为。

那么这个玩具有什么意义嘛？我们并没有脱离真实的操作系统，而是“简化” 了操作系统的 API，在暂时不要过度关注细节的时候理解操作系统。

细节也会有的，但不是现在，这是一个合适的学习路线：先 100% 理解玩具，再理解真实系统和玩具的差异

void sys_write(const char *s) { printf("%s", s); }
void sys_sched() { usleep(rand() % 10000); }
int sys_choose(int x) { return rand() % x; }

void sys_spawn(void *(*fn)(void *), void *args) {
    pthread_create(&threads[nthreads++], NULL, fn, args);
}

C实现的细节，我们希望在 main 之前执行一些代码，在 main 之后也执行一些代码，一些机制后面查资料

学习的方法。不管学什么/

先100%把一个简化的东西理解了，然后再去理解简化的东西和真实的东西的差异，这样在理解真实的东西就不那么困难了。

比如，现在的玩具操作系统，或者早期版本的linux0.11，

或者不妨去看看 RTOS，这就是一个现在在用的几千行的操作系统，跑在嵌入式设备上。

玩具 plus

代码量上来，看看500行可以做成什么样子？

进程+线程+终端+存储(崩溃一致性)

简单理解，线程是可以共享内存的进程。

系统调用	Linux 对应	行为
sys_spawn(fn)	pthread_create	创建从 fn 开始执行的线程
sys_fork()	fork	创建当前状态机的完整复制
sys_sched()	定时被动调用	切换到随机的线程/进程执行
sys_choose(xs)	rand	返回一个 xs 中的随机的选择
sys_write(s)	printf	向调试终端输出字
sys_bread(k)	read	读取虚拟设磁盘块
sys_bwrite(k, v)	write	向虚拟磁盘块
sys_sync()	sync	将所有向虚拟磁盘的数据写入落盘
sys_bwrite(k, v)	write	向虚拟磁盘块
sys_crash()	长按电源按键	模拟系统崩溃

这里还涉及到了磁盘，假象的磁盘，按照块来读写。今天的磁盘，程序说写了不代表真的写进去了。

U盘复制进去立马拔掉，数据可能会丢失，再插上提示是否修复，windows 用了比较保守的策略。

U盘的flash 速度跟不上磁盘，内部自己有个 RAM，一个现象刚开始读写很快，有缓存就意味着，这个时候拔掉U盘，数据就不会按照我们的想法写入。

此外模型作出的简化

• 被动进程/线程切换

  • 实际程序随时都可能被动调用 sys_sched() 切换

• 只有一个终端

  • 没有 read() (用 choose 替代 “允许读到任意值”)

• 磁盘是一个 dict

  • 把任意 key 映射到任意 value

  • 实际的磁盘

    • key 为整数

    • value 是固定大小 (例如 4KB) 的数据

    • 二者在某种程度上是可以 “互相转换” 的

模型实现原理与刚才的 “最小操作系统玩具” 类似，mosaic.py - 500 行建模操作系统

• 进程/线程都是 Generator Object

• 共享内存用 heap 变量访问

• 线程会得到共享 heap 的指针

• 进程会得到一个独立的 heap clone

更重要的，我们是为了输出程序运行的 “状态图”

可以直观地理解程序执行的全流程，可以对照程序在真实操作系统上的运行结果，这对于更复杂的程序来说是十分关键的。