2020/08/04

2020/08/04

# 研究目的

  • OSの信頼性を保証する必要がある
  • 信頼性の保証にはモデル検査や定理証明を使用したい
    • 継続ベースの状態遷移系で再実装することで表現しやすくしたい
  • 既存のunixであるxv6をCbCで書き換えて、検証を行いやすくしたい
    • kernel/user両方をCbCで実装する

# 進捗

  • lock周りの実装を調査していた
    • Gears
    • xv6
    • spinlock的なものをkernel_contextに実装したい
  • シス管関係
    • B1と一緒に作業したり
    • 障害復旧したり
    • 学科サイトからHTMLをgoroutineでダウンロードするくんを書いていたりした
  • 今週はあまり対馬の民を救っていない

# Lock

  • kernel_contextの値を取る時に必要そう
    • 計算に必要なタイミングでstubでkernel_cotnextから回収して、計算が終わったら書き戻す
    • 書き戻す用のmetaが必要そう
  • 想像図
    • lockが取れていたら実際に取り出したいstubにgoto
    • ダメそうならwaitを再帰呼び出し
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
__code consoleread2ReadSyscallImpl(struct ReadSyscallImpl* read_syscall,struct InputArg* input, struct inode* ip, __code next(...)) {
    if (input->r == input->w) {
        if (proc->killed) {
            release(&input->lock);
            ilock(ip);
            KernelRet* kernel_ret = createKernelRetImpl(cbc_context);
            goto kernel_ret->cbc_return(-1);
        }
       goto cbc_sleep(&input->r, &input->lock, cbc_consoleread2);
    }
    goto read_sycall->consoleread1();
}


__code consoleread2ReadSyscallImpl_stub(struct Context* cbc_context) {
   ReadSyscallImpl* read_syscall = (ReadSyscallImpl*)GearImpl(cbc_context, ReadSyscall, read_syscall);
   inode* ip = Gearef(cbc_context, ReadSyscall)->ip;
   enum Code next = Gearef(cbc_context, ReadSyscall)->next;
   struct InputArg* input = GeareData(kernel_context, InputArg);
   goto consoleread2ReadSyscallImpl(cbc_context, read_syscall, ip, next);
}

__code consoleread2ReadSyscallImpl_wait_lock(struct Context* cbc_context) {
   srtruct KernelContext* kcontext = &kernel_context;
   goto semaphore->p(consoleread2ReadSyscallImpl);
}
  • 従来のGears
    • pthreadのAPIを使って実装されている
    • xv6には当然そのまま移植できない
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
__code pOperationSemaphoreImpl(struct SemaphoreImpl* semaphore, __code next(...)) {
    pthread_mutex_lock(&semaphore->mutex);
    goto meta(context, C_pOperationSemaphoreImpl1);
}

__code pOperationSemaphoreImpl1(struct SemaphoreImpl* semaphore, __code next(...)) {
    if (semaphore->value == 0) {
        pthread_cond_wait(&semaphore->cond, &semaphore->mutex);
        goto meta(context, C_pOperationSemaphoreImpl1);
    }
    semaphore->value--;
    pthread_mutex_unlock(&semaphore->mutex);
    goto next(...);
}
  • xv6で実装する場合

    • 我々にはspinlockがあるので…
    • 似たようなlock機能をkernel_context向きに実装するのが早そう
    • なのでxv6のspinlockの実装を眺めていた
  • ロックを獲得するacquire読んだけど#if 0でほとんど使われてなさそう

    • どうも#if 0なのはx86向きのもとコードっぽいxhcgとか使ってるし…..
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
// Acquire the lock.
// Loops (spins) until the lock is acquired.
// Holding a lock for a long time may cause
// other CPUs to waste time spinning to acquire it.
void acquire(struct spinlock *lk)
{
    pushcli();    // disable interrupts to avoid deadlock.
    lk->locked = 1; // set the lock status to make the kernel happy

#if 0
    if(holding(lk))
        panic("acquire");

    // The xchg is atomic.
    // It also serializes, so that reads after acquire are not
    // reordered before it.
    while(xchg(&lk->locked, 1) != 0)
        ;

    // Record info about lock acquisition for debugging.
    lk->cpu = cpu;
    getcallerpcs(get_fp(), lk->pcs);

#endif
}
  • 呼ばれているpush/pop cli
    • みたところint_enabledを読んだあとにcliする世界
    • cpu->nclipushcliのネストということらしい
  • intenaはinterrupt enableの略っぽい
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
// Pushcli/popcli are like cli/sti except that they are matched:
// it takes two popcli to undo two pushcli.  Also, if interrupts
// are off, then pushcli, popcli leaves them off.

void pushcli (void)
{
    int enabled;

    enabled = int_enabled();

    cli();

    if (cpu->ncli++ == 0) { // == cpu->nli == 0; cpu->nlic++
        cpu->intena = enabled;
    }
    
    
}

void popcli (void)
{
    if (int_enabled()) {
        panic("popcli - interruptible");
    }

    if (--cpu->ncli < 0) {
        cprintf("cpu (%d)->ncli: %d\n", cpu, cpu->ncli);
        panic("popcli -- ncli < 0");
    }

    if ((cpu->ncli == 0) && cpu->intena) {
        sti();
    }
}
1
2
3
4
5
6
7
8
9
void cli (void)
{
    uint val;

    // ok, enable paging using read/modify/write
    asm("MRS %[v], cpsr": [v]"=r" (val)::);
    val |= DIS_INT;
    asm("MSR cpsr_cxsf, %[v]": :[v]"r" (val):);
}

# 障害復旧

  • 停電後の復電時に瞬電かなんかでL3スイッチの3つのうち1つが死ぬ
    • 死んだL3に接続していた6Fのフロアスイッチ、6F研究室の多めのやつなどが死
  • 業者の方がいい感じに死んだL3スイッチに接続していたポートを残り2つに移動させていた
Licensed under CC BY-NC-SA 4.0
comments powered by Disqus
Built with Hugo
Theme Stack designed by Jimmy