【06-并发控制：互斥 (1)-课堂示例代码运行】 modelchecker的使用封装 Peterson算法的修改和验证

2024 南京大学 “操作系统：设计与实现” (蒋炎岩) 06-并发控制：互斥 (1)

model checker 的使用（lecture 04）

why using model checker？
——调度就是状态机选择的不确定性

这是第四节课的内容，但我是跳着听的，所以在这里（lecture 06）记录一下。

首先需要python3.9的环境。（我的虚拟机从3.6->3.7->3.8，但apt安装3.9的时候说找不到安装包，所以下载了源代码来安装。btw：如果你遇到了no module named ‘apt_pkg‘这个问题，或许可以参考这篇文章来解决）

然后输入python3.9 mosaic.py +你要检查的代码的路径与文件名就可以了

输出是一个json文件：

然后还可以用管道的方式再精简一下输出：

kimi解释一下这条命令：

1. python3.9 mosaic.py -c examples/intro/hello.py：

   • 这是命令的开始部分，它调用了Python 3.9解释器来执行一个名为mosaic.py的Python脚本。
   • -c 参数后面跟着的是一个字符串，这个字符串是作为Python代码传递给mosaic.py脚本执行的。在这个例子中，传递的代码是examples/intro/hello.py，这通常意味着hello.py是一个Python脚本文件，其内容被当作代码字符串传递给mosaic.py。

2. | grep stdout：

   • grep是一个强大的文本搜索工具，它用于搜索包含特定模式的行。
   • 在这个命令中，grep stdout用于搜索包含单词“stdout”的行。这意味着它会过滤掉python3.9 mosaic.py -c examples/intro/hello.py命令的输出，只留下包含“stdout”的那些行。

3. | sort：

   • sort命令用于将输入的文本行进行排序（默认是按照字典顺序）。
   • 这个命令会将grep stdout的输出结果进行排序。

4. | uniq：

   • uniq命令用于去除排序后的文本中的重复行。
   • 这个命令会将sort命令的输出结果中连续重复的行合并，只保留第一次出现的行。

综上所述，整个命令的作用是：执行mosaic.py脚本，传递hello.py作为代码参数，然后过滤出包含“stdout”的输出行，对这些行进行排序，并去除重复的行。这通常用于清理和简化输出，使得结果更加易于阅读和分析。

以上就是model checker的使用了。

将model checker封装为能直接使用的小工具

这个在lecture 06中老师直接使用了。我通过询问ai得到了步骤。

记录一下：

0. 找到python3.9的路径
   

1. 将脚本制作成可执行文件：

   • 修改了 mosaic.py 文件，使其成为可以直接执行的脚本。即在文件开头添加一个“shebang”行，比如 #!/usr/local/bin/python3.9，这告诉系统使用 python3.9 来执行这个脚本。
   • 
   • 然后，通过在终端中运行 chmod +x mosaic.py 命令，使 mosaic.py 文件变得可执行。至此，就可以用./mosaic.py examples/intro/hello.py 来运行了。

2. 复制到系统的 PATH 中：

   • 为了让 mosaic 命令在任何目录下都能被调用，需要将它复制到系统 PATH 中的一个目录里。PATH 是操作系统用来查找可执行文件的目录列表。
   • 常用的 PATH 目录包括 /usr/local/bin、/usr/bin 等。

     sudo cp mosaic.py /usr/local/bin/mosaic
     

   • 这样，mosaic 就成为了一个全局可用的命令。

可以使用了。

peterson.c的运行

把第五节课示例代码“最小线程库”给的thread.h复制到peterson目录下，把peterson.c中的#include<thread.h>改为#include “thread.h”，makefile改两处：

• 第三行加上 -lpthread
• 第六行把$(CFLAGS)位置调整到最后
  

这样就可以make成功了。

此外你会发现变量TLIB_PATH是空的，这个是正常的。这个变量通常用于告诉编译器在哪里找到特定的库文件（尤其是那些不在标准库路径中的文件）

Peterson.py运行测试

老师在py代码中写的1和2是黑圈形式的，但是我的运行的时候我都的机器分不开这俩标签特殊符号。所以我把代码中改为了普通ascii字符1和2

思考题

先贴标签再举旗

如何修改代码：

正确性：❌
model checker检查截图：

我的解释：
A和B同时贴上了标签，但还都没举旗，那么根据判断条件，只要发现对方没举旗，无论门上是不是自己的名字，都会进。所以❌

结束时撕去门上字条（放下旗子前）

如何修改代码：

正确性：✔
model checker检查截图：

我的解释：A结束后，还举着旗子，但把门上自己的名字撤走。对于B来说不能进。A放下旗子后能进。没有错误。

结束时撕去门上字条（放下旗子后）

如何修改代码：（while的最后加上这两句）

正确性：✔
model checker检查截图：

先观察对方是否举旗，再观察门上标签

如何修改代码：

正确性：✔
model checker检查截图：

我的解释：A先举起来，B看到A举了。B贴上了A的名字，B观察，不能进。A贴上后观察，发现门上是自己的名字，所以进去了。不会出现同时进去的问题。

是否存在都进不去or不公平的情况？

还不知道

使用原子指令实现求和

还是CFLAGS换一下位置，如果TLIB为空，那么把-I删掉

thread.h放到sum文件夹下

我的虚拟机设置的核数为1，所以加不加lock结果都是对的（且都很慢）
当设置核数为2时，看到了期待的结果。

不加lock：

加lock：