Mercurial > hg > Document > Growi

view user/anatofuz/note/2021/01/19.md @ 27:459b9fa6f047

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
backup 2021-01-20
author autobackup
date Wed, 20 Jan 2021 00:10:03 +0900
parents
children
line wrap: on
line source



# 研究目的
- アプリケーションの信頼性を保証するには土台となるOSの信頼性を高く保証する必要がある
    - しかしOSの機能をテストですべて検証するのは不可能である。
- 定理証明やモデル検査を利用して、テストに頼らずに保証したい
    - 証明しやすい形、かつ実際に動くソースコードが必要
    - 継続ベースの状態遷移系で再実装することで表現しやすくしたい
- プログラムは二つの計算に分離される
    - プログラムは入力と出力の関係を決める計算(ノーマルレベル)
    - その計算に必要なメタな計算(メタレベル)
- プログラムの信頼性の保証を動作しつつ行うには、メタレベルの計算を活用したい
- そのためにはメタレベルの計算を柔軟に扱うAPIや, メタレベルを保証しつつCbCを拡張した実装方法が必要
- 本研究ではノーマル/メタレベルでの実装に適した、継続を基本とする言語Continuation Based Cを用いて、OSの実装を行い、メタ計算APIについて考察する。


# 今週
- genericsの実装あとすこし
- DPPの例題をちょいちょい修正
- 学位審査願いを提出する必要があるらしい
- シス管とか...

# generics
- 型と`.cbc`の書き換えを行う方針
    - どの型を生成したか覚える必要があるので、`generete_context`でまとめて変換

# genericsの使い方
- 型変数として使っているケース
- 型変数に具体的な値をいれているところ(型インスタンス)
- interfaceの実装にgenericsが伝搬するケース
    - しないケース

## 型変数として使っているケース

- この場合は`T`は型変数

```c
typedef struct AtomicT <T>{
    __code checkAndSet(Impl* atomic_t,T* ptr ,T init, T newData, __code next(...), __code fail(...));
    __code set(Impl* atomic_t,T* ptr ,T newData, __code next(...));
    __code next(...);
    __code fail(...);
} AtomicT;
```

## 型インスタンス

- Tに具体的な値`int`を埋め込んでいる

```c
typedef struct PhilsImpl <> impl Phils {
  int self;
  AtomicT<int> Leftfork;
  AtomicT<int> Rightfork;
  __code next(...);
} PhilsImpl;
```

## interfaceの実装にgenericsが伝搬するケース

- 型変数Tが共通
   - implが決まればinterfaceも決まる

```c
typedef struct AtomicT <T>{
    __code checkAndSet(Impl* atomic_t,T* ptr ,T init, T newData, __code next(...), __code fail(...));
    __code set(Impl* atomic_t,T* ptr ,T newData, __code next(...));
    __code next(...);
    __code fail(...);
} AtomicT;
```

```c
typedef struct AtomicTImpl <T> impl AtomicT {
  T atomic;
  T init;
  __code next(...);
} AtomicTImpl;
```

## interfaceの実装にgenericsが伝搬しないケース

- inputDataGearとしてはTはくる
    - stack_generics_impl自体はTは持たない(stack_generics_impl.cbcはもつ

```c
typedef struct StackGenerics <T> {
    __code clear(Impl* stack,__code next(...));
    __code push(Impl* stack,T* data, __code next(...));
    __code pop(Impl* stack, __code next(T* data, ...));
    __code pop2(Impl* stack, __code next(T* data, T* data1, ...));
    __code isEmpty(Impl* stack, __code next(...), __code whenEmpty(...));
    __code get(Impl* stack, __code next(T* data, ...));
    __code get2(Impl* stack, __code next(T* data, T* data1, ...));
    __code next(...);
    __code whenEmpty(...);
} StackGenerics;
```

```
typedef struct StackGenericsImpl <T> impl StackGenerics {
  __code next(...);
} StackGenericsImpl;
```

# .cbcに関する話
- `AtomicT<int>`みたいに使っている場所はわかりやすく置換
- `AtomicT<T>`を作るimplなCbCファイルはgenericsで使われている値が決まったら、その分だけ作る
    - `AtomicT<int>, AtomicT<foo>` -> `AtomicT_int`, `AtomicT_foo`をつくる
    - `.cbc`の中身を一度よむ -> 書き換えをする必要がある


# 現状

- 誰がどこでgenericsを使っているかは特定
- 型インスタンス的に使っているとこの書き換えが完了
- implのcbcの書き換えを今実装中
- ヘッダはcontextを作る前に差し替える

```perl
[
    [0] {
        AtomicT       {
            _caller   {
                /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/AtomicT.h   1
            },
            T         [
                [0] "ptr",
                [1] "init",
                [2] "newData"
            ]
        },
        AtomicTImpl   {
            _caller      {
                /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/AtomicTImpl.c                       1,
                /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/AtomicTImpl.h   1
            },
            _interface   "AtomicT",
            T            [
                [0] "atomic",
                [1] "init",
                [2] "AtomicT"
            ]
        }
    },
    [1] {
        AtomicT   {
            int   [
                [0] {
                    caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h",
                    impl           "PhilsImpl",
                    inCbC          0,
                    interface      "Phils",
                    in_type_name   "PhilsImpl",
                    vname          "Leftfork"
                },
                [1] {
                    caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h",
                    impl           "PhilsImpl",
                    inCbC          0,
                    interface      "Phils",
                    in_type_name   "PhilsImpl",
                    vname          "Rightfork"
                },
                [2] {
                    caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c",
                    impl           "PhilsImpl",
                    inCbC          1,
                    interface      "Phils",
                    in_type_name   "AtomicT",
                    vname          "right"
                },
                [3] {
                    caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c",
                    impl           "PhilsImpl",
                    inCbC          1,
                    interface      "Phils",
                    in_type_name   "AtomicT",
                    vname          "left"
                },
                [4] {
                    caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c",
                    impl           "AtomicTImpl",
                    inCbC          1,
                    interface      "AtomicT",
                    in_type_name   "AtomicT",
                    vname          "AtomicT"
                },
                [5] {
                    caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c",
                    impl           "AtomicTImpl",
                    inCbC          1,
                    interface      "AtomicT",
                    in_type_name   "AtomicT",
                    vname          "AtomicT"
                },
                [6] {
                    caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c",
                    impl           "AtomicTImpl",
                    inCbC          1,
                    interface      "AtomicT",
                    in_type_name   "AtomicT",
                    vname          "AtomicT"
                },
                [7] {
                    caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c",
                    impl           "AtomicTImpl",
                    inCbC          1,
                    interface      "AtomicT",
                    in_type_name   "AtomicT",
                    vname          "AtomicT"
                },
                [8] {
                    caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c",
                    impl           "AtomicTImpl",
                    inCbC          1,
                    interface      "AtomicT",
                    in_type_name   "AtomicT",
                    vname          "AtomicT"
                }
            ]
        }
    }
]
```

# ここから下は作業メモ

```perl
\ {
    AtomicT       {
        file_path              "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/AtomicT.h",
        name                   "AtomicT",
        typed_variable         [
            [0] {
                type    "T",
                vname   "ptr"
            },
            [1] {
                type    "T",
                vname   "init"
            },
            [2] {
                type    "T",
                vname   "newData"
            }
        ],
        typed_variable_types   {
            T   [
                [0] "ptr",
                [1] "init",
                [2] "newData"
            ]
        }
    },
    AtomicTImpl   {
        file_path              "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/AtomicTImpl.h",
        interface              "AtomicT",
        name                   "AtomicTImpl",
        typed_variable         [
            [0] {
                type    "T",
                vname   "atomic"
            },
            [1] {
                type    "T",
                vname   "init"
            }
        ],
        typed_variable_types   {
            T   [
                [0] "atomic",
                [1] "init"
            ]
        }
    }
}
\ {
    AtomicT     {
        caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c",
        defined_type   "int",
        line_number    14,
        name           "AtomicT"
    },
    PhilsImpl   {
        field_defined_type   [
            [0] {
                generics   "int",
                type       "AtomicT",
                vname      "Leftfork"
            },
            [1] {
                generics   "int",
                type       "AtomicT",
                vname      "Rightfork"
            }
        ],
        file_path            "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h",
        interface            "Phils",
        name                 "PhilsImpl"
    }
}
```


```perl
\ {
    StackGenerics   {
        file_path              "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/interface/StackGenerics.h",
        name                   "StackGenerics",
        typed_variable         [
            [0] {
                type    "T",
                vname   "data"
            },
            [1] {
                type    "T",
                vname   "data1"
            }
        ],
        typed_variable_types   {
            T   [
                [0] "data",
                [1] "data1"
            ]
        }
    }
}
\ {
    StackGenerics   {
        caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/generics_test/main.c",
        defined_type   "Integer",
        line_number    49,
        name           "StackGenerics"
    }
}
```



# フロー
- `AtomicT<int>`している箇所を特定
    - `.h`と`.cbc`
      - それぞれ置換していく(rename)
- `AtomicT<T>`を使っている箇所を特定
    - `.h`と`.cbc`
    - この場合は本体を削除して置き換える
        - 具体的なinstanceの数分作成する
- 知らないと行けないのは?
    - 置換すべきファイル名
    - InterfaceかImplか
        - implだったらinterfaceも書き換え?
            - 同じファイルかチェックする必要がありそう
    - 置換する対象
        - フィールド
        - 型名
        - CodeGearの名前


# 処理自体は

```shell
$cat c/AtomicTImpl.c | perl -nle 's/<.*>//g; s/AtomicT/AtomicTInt/g; s/(AtomicT\w+)Impl/$1ImplInt/g;print'
```


```perl
\ {
    StackGenerics   {
        Integer   [
            [0] {
                caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/generics_test/main.c",
                impl           "StackGenericsImpl",
                inCbC          1,
                interface      "StackGenerics",
                in_type_name   "StackGenerics",
                vname          "StackGenerics"
            }
        ]
    }
}
\ {
    StackGenerics   {
        _caller   {
            /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/interface/StackGenerics.h   1
        },
        T         [
            [0] "data",
            [1] "data1"
        ]
    }
}
```


```
[
    [0] {
        StackGenerics   {
            _caller   {
                /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/interface/StackGenerics.h   1
            },
            T         [
                [0] "data",
                [1] "data1"
            ]
        }
    },
    [1] {
        StackGenerics   {
            Integer   [
                [0] {
                    caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/generics_test/main.c",
                    impl           "StackGenericsImpl",
                    inCbC          1,
                    interface      "StackGenerics",
                    in_type_name   "StackGenerics",
                    vname          "StackGenerics"
                }
            ]
        }
    }
]
```


```
+kajika+anatofuz$ ./dpp_create_context.sh > /dev/null
\ {
    /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c                            [
        [0] {
            caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c",
            impl           "AtomicTimpl",
            inCbC          1,
            interface      "AtomicT",
            in_type_name   "AtomicT",
            vname          "AtomicT"
        },
        [1] {
            caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c",
            impl           "AtomicTimpl",
            inCbC          1,
            interface      "AtomicT",
            in_type_name   "AtomicT",
            vname          "AtomicT"
        },
        [2] {
            caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c",
            impl           "AtomicTimpl",
            inCbC          1,
            interface      "AtomicT",
            in_type_name   "AtomicT",
            vname          "AtomicT"
        },
        [3] {
            caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c",
            impl           "AtomicTimpl",
            inCbC          1,
            interface      "AtomicT",
            in_type_name   "AtomicT",
            vname          "AtomicT"
        },
        [4] {
            caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/main.c",
            impl           "AtomicTimpl",
            inCbC          1,
            interface      "AtomicT",
            in_type_name   "AtomicT",
            vname          "AtomicT"
        }
    ],
    /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c                       [
        [0] {
            caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c",
            impl           "PhilsImpl",
            inCbC          1,
            interface      "Phils",
            in_type_name   "AtomicT",
            vname          "right"
        },
        [1] {
            caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/c/examples/DPP/PhilsImpl.c",
            impl           "PhilsImpl",
            inCbC          1,
            interface      "Phils",
            in_type_name   "AtomicT",
            vname          "left"
        }
    ],
    /home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h   [
        [0] {
            caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h",
            impl           "PhilsImpl",
            inCbC          0,
            interface      "Phils",
            in_type_name   "PhilsImpl",
            vname          "Leftfork"
        },
        [1] {
            caller         "/home/anatofuz/src/firefly/hg/Gears/Gears/src/parallel_execution/../parallel_execution/examples/DPP/PhilsImpl.h",
            impl           "PhilsImpl",
            inCbC          0,
            interface      "Phils",
            in_type_name   "PhilsImpl",
            vname          "Rightfork"
        }
    ]
}
```