当前位置: 首页 > article >正文

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

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

文章目录

    • model checker 的使用(lecture 04)
    • 将model checker封装为能直接使用的小工具
    • peterson.c的运行
    • Peterson.py运行测试
      • 思考题
        • 先贴标签再举旗
        • 结束时撕去门上字条(放下旗子前)
        • 结束时撕去门上字条(放下旗子后)
        • 先观察对方是否举旗,再观察门上标签
        • 是否存在都进不去or不公平的情况?
    • 使用原子指令实现求和

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得到了步骤。
在这里插入图片描述

记录一下:

  1. 找到python3.9的路径
    在这里插入图片描述

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

    • 修改了 mosaic.py 文件,使其成为可以直接执行的脚本。即在文件开头添加一个“shebang”行,比如 #!/usr/local/bin/python3.9,这告诉系统使用 python3.9 来执行这个脚本。
    • 在这里插入图片描述
    • 然后,通过在终端中运行 chmod +x mosaic.py 命令,使 mosaic.py 文件变得可执行。至此,就可以用./mosaic.py examples/intro/hello.py 来运行了。
  3. 复制到系统的 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:
在这里插入图片描述


http://www.kler.cn/a/371359.html

相关文章:

  • 探熵科技|以科技赋能销售,创造卓越业绩。
  • 泛微开发修炼之旅--48关于ecology重写消息卡片中的创建时间和创建人的解决方案及源码
  • Python 爬虫的寻宝大冒险:如何捕获 API 数据的宝藏
  • Spring Boot框架中小企业设备监控系统开发
  • 八,Linux基础环境搭建(CentOS7)- 安装Mysql和Hive
  • DBeaver如何导出insert的sql数据
  • 迈威通信西安采矿展大放异彩,驱动煤矿智能转型加速跑
  • 面试中的一个基本问题:如何在数据库中存储密码?
  • Codeforces Round 909 (Div. 3)
  • selenium解决调用Chrome str’ object has no attribute ‘capabilities’ Process finished
  • redis修改配置文件配置密码开启远程访问后台运行
  • Vscode中Github Copilot无法使用
  • 攻防世界的新手web题解
  • web前端多媒体标签设置(图片,视频,音频)以及图片热区(usemap)的设置
  • C++:多态(原理篇)
  • 交流调速系统分类
  • 如何从PPT中导出600dpi的高清图
  • 在 Vue 中如何自动导入项目中的 less 和 scss 变量和文件
  • macOS开发环境配置与应用开发教程
  • java 泛型返回接口
  • vue使用rem适配各种分辨率设备
  • 【PTA】4-2 树的同构【数据结构】
  • 鸿蒙的底部菜单导航实现
  • appium自动化对已打开的app操作
  • pdf转为txt文本格式并使用base64加密输出数据
  • 事务的原理、MVCC的原理