文件名称：habanero-coq：Habanero编程模型的Coq形式化
文件大小：154KB
文件格式：ZIP
更新时间：2024-02-24 18:14:34
synchronization phaser coq parallel-computing coq-formalization
Habanero编程模型的Coq形式化 编程模型的形式化。 我们主要关注属性的形式化，例如死锁*和种族*。 该项目的总体目标是提供理论框架，阅读Coq库，以验证同步机制。 刊物 使用Coq对Habanero移相器进行形式化。 Tiago Cogumbreiro，Jun Shirako和Vivek Sarkar。 JLAMP，90：50–60，2017年。 相序的形式化。 Tiago Cogumbreiro，Jun Shirako和Vivek Sarkar。 在PLACES'16的会议记录中，2016。 总览 我们目前正在努力： 移相器操作的无死锁子集 异步完成 使用 确保已安装 。
【文件预览】：
habanero-coq-master
----_CoqProject(601B)
----push-all.sh(181B)
----generate-html.sh(117B)
----src()
--------Vars.v(825B)
--------Tid.v(3KB)
--------CG.v(4KB)
--------All.v(33KB)
--------Finish()
--------Phasers()
--------Bijection.v(12KB)
--------Fid.v(3KB)
--------Node.v(12KB)
--------ReverseSemaphore.v(6KB)
----ocaml()
--------main.mli(0B)
--------cstruct.js(2KB)
--------myocamlbuild.ml(70B)
--------jquery.js(85KB)
--------_tags(76B)
--------Makefile(750B)
--------.gitignore(106B)
--------main.ml(8KB)
----configure.sh(557B)
----libhsem()
--------codegen()
--------src()
--------lib()
--------configure.sh(69B)
--------myocamlbuild.ml(4KB)
--------_tags(437B)
--------test()
--------README.md(882B)
--------Makefile(987B)
--------.gitignore(47B)
--------bin()
----.travis.yml(905B)
----LICENSE(1KB)
----README.md(2KB)
----coqide.sh(33B)
----.gitignore(95B)
----.gitlab-ci.yml(571B)