OS

操作系统课程2024-04

数学视角的操作系统

Posted by BY morningcat on May 13, 2024

程序正确性证明

  • 暴力枚举
  • 写出证明

暴力枚举带来的启发

  • 我们应该把需要证明的性质写成 assertions

写出证明带来的启发

  • 容易阅读 (self-explain) 的代码是好代码
  • 容易验证 (self-evident) 的代码是好代码

进入BIOS

  1. windows

疑难问题 》 高级选项 》 UEFI 固件设置

  1. F10 or DEL

  2. 命令行

shutdown /r /o /t 0

OS 模型

#!/usr/bin/env python3
# os-model.py

import sys
import random
from pathlib import Path

class OS:
    '''
    A minimal executable operating system model. Processes
    are state machines (Python generators) that can be paused
    or continued with local states being saved.
    '''

    '''
    We implement four system calls:

    - read: read a random bit value.
    - write: write a string to the buffer.
    - spawn: create a new state machine (process).
    '''
    SYSCALLS = ['read', 'write', 'spawn']

    class Process:
        '''
        A "freezed" state machine. The state (local variables,
        program counters, etc.) are stored in the generator
        object.
        '''

        def __init__(self, func, *args):
            # func should be a generator function. Calling
            # func(*args) returns a generator object.
            self._func = func(*args)

            # This return value is set by the OS's main loop.
            self.retval = None

        def step(self):
            '''
            Resume the process with OS-written return value,
            until the next system call is issued.
            '''
            syscall, args, *_ = self._func.send(self.retval)
            self.retval = None
            return syscall, args

    def __init__(self, src):
        # This is a hack: we directly execute the source
        # in the current Python runtime--and main is thus
        # available for calling.
        exec(src, globals())
        self.procs = [OS.Process(main)]
        self.buffer = ''

    def run(self):
        # Real operating systems waste all CPU cycles
        # (efficiently, by putting the CPU into sleep) when
        # there is no running process at the moment. Our model
        # terminates if there is nothing to run.
        while self.procs:

            # There is also a pointer to the "current" process
            # in today's operating systems.
            current = random.choice(self.procs)

            try:
                # Operating systems handle interrupt and system
                # calls, and "assign" CPU to a process.
                match current.step():
                    case 'read', _:
                        current.retval = random.choice([0, 1])
                    case 'write', s:
                        self.buffer += s
                    case 'spawn', (fn, *args):
                        self.procs += [OS.Process(fn, *args)]
                    case _:
                        assert 0

            except StopIteration:
                # The generator object terminates.
                self.procs.remove(current)

        return self.buffer

if __name__ == '__main__':
    if len(sys.argv) < 2:
        print(f'Usage: {sys.argv[0]} file')
        exit(1)

    src = Path(sys.argv[1]).read_text()

    # Hack: patch sys_read(...) -> yield "sys_read", (...)
    for syscall in OS.SYSCALLS:
        src = src.replace(f'sys_{syscall}',
                          f'yield "{syscall}", ')

    stdout = OS(src).run()
    print(stdout)

# hello.py
def main():
    x = 0
    for _ in range(10):
        b = sys_read()
        x = x * 2 + b

    sys_write(f'x = {x:010b}b')

python3 os-model.py hello.py