changeset 32:966737d7c80a

backup 2021-01-25
author autobackup
date Mon, 25 Jan 2021 00:10:03 +0900
parents 38ca0355d32c
children 7d7f7fffd8fa
files user/Okud/メモ/2021/01/24.md user/anatofuz/note/2021/01/24.md
diffstat 2 files changed, 185 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/Okud/メモ/2021/01/24.md	Mon Jan 25 00:10:03 2021 +0900
@@ -0,0 +1,37 @@
+# Gears OS Device Driver 作成
+## 研究目的
+- 当研究室では,OSの信頼性と拡張性をテーマにGearsOSの開発をしている。
+- 時代と共にハードウェア、サービスが進歩していき、その度に OS を検証できる必要があるため、拡張性が必要。
+- OS は非決定的な実行を持ち、従来の OS ではテストしきれない部分が残ってしまうため、信頼性が欠けてしまうので信頼性のある OS が必要。
+- GearsOSは,信頼性をノーマルレベルの計 算に対して保証し、拡張性をメタレベルの計算で実現することを目標に設計している。
+- GearsOSは,Continuation based C(CbC)によってアプリケーションとOSそのものを記述している。
+- CbCは,Code Gear と Data Gearの単位でプログラムを記述する。
+- Code Gearは並列処理の単位として利用でき、Data Gear はデータそのもので型を持っていて、CbC はメタレベルの処理,並列処理を記述することができる。
+- 本研究では,ARMで動くシングルコンピュータであるRaspberryPi上にUEFIからGearsOSをbootして、GearsOSのデバイスドライバを作成し,ハードウェア上でもメタレベルの処理、並列実行ができるプログラミングを記述できるようになる事を目指している。
+- 
+
+## 進捗
+- xv6をRaspberryPiのUEFIからbootさせる
+    - xv6はUEFIからbootできない
+    - 自作のbootloaderが必要
+    - x86-64のbootloaderがある
+        - 試した結果動かない
+        - ![bootload_error.png](/attachment/600d30b485cd4400490076ba)
+        - この画面が出てり消えたり
+        - logo.bmpが開けないらしい
+    - QEMUで動かしたaarchのUEFIはRaspberryPi3の環境では動かない
+        - qemuのマシンにrasp3を追加した
+        ```
+        shine@KokinoMacBook-Pro thesis % qemu-system-aarch64 -M help | grep rasp 
+        ```
+        ```
+        raspi2               Raspberry Pi 2B
+        raspi3               Raspberry Pi 3B
+        ```
+        - -M rasp3(ラズパイ3マシンを使う)
+        - RPI_EFI.FDではUEFIが起動しない
+            - FDファイルを自分で作る必要がある
+        - qemuのオプションに何があるかまだわかってない
+        
+
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/user/anatofuz/note/2021/01/24.md	Mon Jan 25 00:10:03 2021 +0900
@@ -0,0 +1,148 @@
+```
++kajika+anatofuz$ perl generate_stub.pl --debug ModelChecking/MCWorker.cbc
+[getDataGear] match 180 : #interface "TaskManager.h"
+[getDataGear] match 141 : typedef struct TaskManager<>{
+[getDataGear] match 343 :   __code spawn(Impl* taskManager, struct Context* task, __code next(...));
+[getDataGear] match 343 :   __code spawnTasks(Impl* taskManagerImpl, struct Element* taskList, __code next1(...));
+[getDataGear] match 343 :   __code setWaitTask(Impl* taskManagerImpl, struct Context* task, __code next(...));
+[getDataGear] match 343 :   __code shutdown(Impl* taskManagerImpl, __code next(...));
+[getDataGear] match 343 :   __code incrementTaskCount(Impl* taskManagerImpl, __code next(...));
+[getDataGear] match 343 :   __code decrementTaskCount(Impl* taskManagerImpl, __code next(...));
+[getDataGear] match 343 :   __code next(...);
+[getDataGear] match 343 :   __code next1(...);
+[getDataGear] match 320 : } TaskManager;
+[getCodeGear] match 398 : typedef struct TaskManager<>{
+[getCodeGear] match 403 :   __code spawn(Impl* taskManager, struct Context* task, __code next(...));
+[getCodeGear] match 403 :   __code spawnTasks(Impl* taskManagerImpl, struct Element* taskList, __code next1(...));
+[getCodeGear] match 403 :   __code setWaitTask(Impl* taskManagerImpl, struct Context* task, __code next(...));
+[getCodeGear] match 403 :   __code shutdown(Impl* taskManagerImpl, __code next(...));
+[getCodeGear] match 403 :   __code incrementTaskCount(Impl* taskManagerImpl, __code next(...));
+[getCodeGear] match 403 :   __code decrementTaskCount(Impl* taskManagerImpl, __code next(...));
+[getCodeGear] match 403 :   __code next(...);
+[getCodeGear] match 403 :   __code next1(...);
+[getDataGear] match 180 : #interface "Worker.h"
+[getDataGear] match 141 : typedef struct Worker<>{
+[getDataGear] match 320 :     union Data* worker;
+[getDataGear] match 320 :     struct Queue* tasks;
+[getDataGear] match 320 :     struct Context* task;
+[getDataGear] match 320 :     pthread_t thread;
+[getDataGear] match 320 :     struct TaskManager* taskManager;
+[getDataGear] match 343 :     __code taskReceive(Impl* worker, struct Queue* tasks);
+[getDataGear] match 343 :     __code shutdown(Impl* worker);
+[getDataGear] match 343 :     __code next(...);
+[getDataGear] match 320 : } Worker;
+[getCodeGear] match 398 : typedef struct Worker<>{
+[getCodeGear] match 403 :     __code taskReceive(Impl* worker, struct Queue* tasks);
+[getCodeGear] match 403 :     __code shutdown(Impl* worker);
+[getCodeGear] match 403 :     __code next(...);
+[getDataGear] match 180 : #interface "Iterator.h"
+[getDataGear] match 141 : typedef struct Iterator<>{
+[getDataGear] match 320 :         union Data* iterator;
+[getDataGear] match 320 :         struct Context* task;
+[getDataGear] match 320 :         int numGPU;
+[getDataGear] match 343 :         __code exec(Impl* iterator, struct Context* task, int numGPU, __code next(...));
+[getDataGear] match 343 :         __code barrier(Impl* iterator, struct Context* task, __code next(...), __code whenWait(...));
+[getDataGear] match 343 :         __code whenWait(...);
+[getDataGear] match 343 :         __code next(...);
+[getDataGear] match 320 : } Iterator;
+[getCodeGear] match 398 : typedef struct Iterator<>{
+[getCodeGear] match 403 :         __code exec(Impl* iterator, struct Context* task, int numGPU, __code next(...));
+[getCodeGear] match 403 :         __code barrier(Impl* iterator, struct Context* task, __code next(...), __code whenWait(...));
+[getCodeGear] match 403 :         __code whenWait(...);
+[getCodeGear] match 403 :         __code next(...);
+[getDataGear] match 180 : #interface "Queue.h"
+[getDataGear] match 141 : typedef struct Queue<>{
+[getDataGear] match 343 :     __code whenEmpty(...);
+[getDataGear] match 343 :     __code clear(Impl* queue, __code next(...));
+[getDataGear] match 343 :     __code put(Impl* queue, union Data* data, __code next(...));
+[getDataGear] match 343 :     __code take(Impl* queue, __code next(union Data* data, ...));
+[getDataGear] match 343 :     __code isEmpty(Impl* queue, __code next(...), __code whenEmpty(...));
+[getDataGear] match 343 :     __code next(...);
+[getDataGear] match 320 : } Queue;
+[getCodeGear] match 398 : typedef struct Queue<>{
+[getCodeGear] match 403 :     __code whenEmpty(...);
+[getCodeGear] match 403 :     __code clear(Impl* queue, __code next(...));
+[getCodeGear] match 403 :     __code put(Impl* queue, union Data* data, __code next(...));
+[getCodeGear] match 403 :     __code take(Impl* queue, __code next(union Data* data, ...));
+[getCodeGear] match 403 :     __code isEmpty(Impl* queue, __code next(...), __code whenEmpty(...));
+[getCodeGear] match 403 :     __code next(...);
+[getDataGear] match 157 : Worker* createMCWorker(struct Context* context, int id, Queue* queue) {
+[getDataGear] match 211 : __code taskReceiveMCWorker(struct MCWorker* worker, struct Queue* tasks) {
+[getDataGear] match 255 :     goto tasks->take(getTaskMCWorker);
+[getDataGear] match 211 : __code startModelChecker(struct MCWorker* worker) {
+[getDataGear] match 245 :     struct SingleLinkedQueue* mcQueue = (struct SingleLinkedQueue*) worker->mcQueue->queue;
+[getDataGear] match 255 :     goto mcQueue->take(meta);
+[AUTOINCLUDE] Forget #interface 'SingleLinkedQueue'  declaration in ModelChecking/MCWorker.cbc at generate_stub.pl line 276.
+[getDataGear] match 141 : typedef struct SingleLinkedQueue <> impl Queue {
+[getDataGear] match 320 :   struct Element* top;
+[getDataGear] match 320 :   struct Element* last;
+[getDataGear] match 320 : } SingleLinkedQueue;
+[getDataGear] match 211 : __code getTaskMCWorker(struct MCWorker* mcWorker, struct Context* task, struct Worker* worker) {
+[getDataGear] match 255 :         goto worker->shutdown(); // end thread
+[getDataGear] match 245 :     struct Queue* mcQueue = mcWorker->mcQueue;
+[getDataGear] match 255 :     goto mcQueue->put(task, taskReceiveMCWorker);
+[getDataGear] match 211 : __code getTaskMCWorker_stub(struct Context* context) {
+[getDataGear] match 211 : __code odgCommitMCWorker(struct MCWorker* worker, struct Context* task) {
+[getDataGear] match 245 :         struct Iterator* iterator = task->iterator;
+[getDataGear] match 255 :         goto iterator->barrier(task, odgCommitMCWorker1, odgCommitMCWorker6);
+[getDataGear] match 211 : __code odgCommitMCWorker_stub(struct Context* context) {
+[getDataGear] match 211 : __code odgCommitMCWorker1(struct MCWorker* worker, struct Context* task) {
+[getDataGear] match 245 :     struct TaskManager* taskManager = task->taskManager;
+[getDataGear] match 255 :     goto taskManager->decrementTaskCount(odgCommitMCWorker6);
+[getDataGear] match 211 : __code odgCommitMCWorker2(struct MCWorker* worker, struct Context* task) {
+[getDataGear] match 245 :     struct Queue* queue = GET_WAIT_LIST(task->data[task->odg+i]);
+[getDataGear] match 255 :     goto queue->isEmpty(odgCommitMCWorker3, odgCommitMCWorker5);
+[getDataGear] match 211 : __code odgCommitMCWorker3(struct MCWorker* worker, struct Context* task) {
+[getDataGear] match 245 :     struct Queue* queue = GET_WAIT_LIST(task->data[task->odg+i]);
+[getDataGear] match 255 :     goto queue->take(odgCommitMCWorker4);
+[getDataGear] match 211 : __code odgCommitMCWorker4(struct MCWorker* worker, struct Context* task, struct Context* waitTask) {
+[getDataGear] match 245 :         struct TaskManager* taskManager = waitTask->taskManager;
+[getDataGear] match 255 :         goto taskManager->spawn(waitTask, odgCommitMCWorker2);
+[getDataGear] match 211 : __code odgCommitMCWorker4_stub(struct Context* context) {
+[getDataGear] match 211 : __code odgCommitMCWorker5(struct MCWorker* worker, struct Context* task) {
+[getDataGear] match 211 : __code odgCommitMCWorker6(struct MCWorker* worker, struct Context* task) {
+[getDataGear] match 245 :     struct Worker* taskWorker = task->worker;
+[getDataGear] match 255 :     goto taskWorker->taskReceive(taskWorker->tasks);
+[getDataGear] match 211 : __code shutdownMCWorker(struct MCWorker* worker) {
+[generateDataGear] match 673 : #include "../../context.h"
+[generateDataGear] match 668 : #interface "TaskManager.h"
+[generateDataGear] match 668 : #interface "Worker.h"
+[generateDataGear] match 668 : #interface "Iterator.h"
+[generateDataGear] match 668 : #interface "Queue.h"
+[generateDataGear] match 801 :
+[generateDataGear] match 801 : static void startWorker(Worker* worker);
+[generateDataGear] match 801 :
+[generateDataGear] match 801 : Worker* createMCWorker(struct Context* context, int id, Queue* queue) {
+[generateDataGear] match 801 :     struct Worker* worker = new Worker();
+[generateDataGear] match 801 :     struct MCWorker* mcWorker = new MCWorker();
+[generateDataGear] match 801 :     mcWorker->mcQueue = createSingleLinkedQueue(context);
+[generateDataGear] match 801 :     worker->worker = (union Data*)mcWorker;
+[generateDataGear] match 801 :     worker->tasks = queue;
+[generateDataGear] match 801 :     mcWorker->id = id;
+[generateDataGear] match 801 :     mcWorker->loopCounter = 0;
+[generateDataGear] match 801 :     worker->taskReceive = C_taskReceiveMCWorker;
+[generateDataGear] match 801 :     worker->shutdown = C_shutdownMCWorker;
+[generateDataGear] match 801 :     pthread_create(&worker->thread, NULL, (void*)&startWorker, worker);
+[generateDataGear] match 801 :     return worker;
+[generateDataGear] match 801 : }
+[generateDataGear] match 801 :
+[generateDataGear] match 801 : static void startWorker(struct Worker* worker) {
+[generateDataGear] match 801 :     struct MCWorker* mcWorker = &worker->worker->MCWorker;
+[generateDataGear] match 801 :     mcWorker->context = NEW(struct Context);
+[generateDataGear] match 801 :     initContext(mcWorker->context);
+[generateDataGear] match 801 :     Gearef(mcWorker->context, Worker)->worker = (union Data*)worker;
+[generateDataGear] match 801 :     Gearef(mcWorker->context, Worker)->tasks = worker->tasks;
+[generateDataGear] match 801 :     goto meta(mcWorker->context, worker->taskReceive);
+[generateDataGear] match 801 : }
+[generateDataGear] match 801 :
+[generateDataGear] match 692 : __code taskReceiveMCWorker(struct MCWorker* worker, struct Queue* tasks) {
+[generateDataGear] match 897 :     goto tasks->take(getTaskMCWorker);
+[generateDataGear] match 1037 : }
+[generateDataGear] match 1061 : }
+[generateDataGear] match 801 :
+[generateDataGear] match 692 : __code startModelChecker(struct MCWorker* worker) {
+[generateDataGear] match 1028 :     struct SingleLinkedQueue* mcQueue = (struct SingleLinkedQueue*) worker->mcQueue->queue;
+[generateDataGear] match 897 :     goto mcQueue->take(meta);
+[ERROR] not found mcQueue definition at     goto mcQueue->take(meta);
+ in ModelChecking/MCWorker.cbc
+```