Blog Archives

20160615

동시성 프로그램의 이해 기말고사 부분 20160405 20160407 20160428 20160503 20160510 20160512 20160524 20160526 20160531 20160602 20160607 20160609 20160614 Advertisements

Tagged with: , , , ,
Posted in 1) Memo

20160614

동시성 프로그램의 이해 – 운영체제의 커널은 테스팅하기가 어렵다. 코드가 복잡하고, 멀티 쓰레드이며, 유닛 테스팅이 어렵고, 테스팅 툴이 부족하다. 유닛 테스팅을 하려면 해당 유닛이 실행되기 위한 환경을 제공해야 한다. 하지만 monolithic kernel에서 하나의 유닛만 떼어내기가 힘들다. 커널은 고성능이어야 하며, 정확해야 한다.

Tagged with: , , , , ,
Posted in 1) Memo

20160609

동시성 프로그램의 이해 – Linear time temporal logic(LTL)은 시간을 상태의 무한한 연속으로 모델링한다(LTL models time as a sequence of states, extending infinitely into the future). LTL에서 x가 항상 2인 상태를 [](x==2)로 표현할 수 있다. LTL을 사용하지 않는다면 x==2@s0, x==2@s1, x==2@s2…와

Tagged with: , , , , , , ,
Posted in 1) Memo

20160607

동시성 프로그램의 이해 – 실제 프로그램과 model checking language 사이에는 차이가 있다. 변환하는 과정에서 오류가 있다면? Model-based testing에서 실제 프로그램을 model checking language로 얼마나 정확하게 변환하느냐는 중요한 문제이다. – Spin에서 statements를 atomic으로 묶으면 interleaving 없이 실행하게 된다. atomic block 중에

Tagged with: , , , , , , , , , , , , , ,
Posted in 1) Memo

20160602

동시성 프로그램의 이해 – Spin에서 “active proctype inv() { assert( x== 0);}”는 모든 경우에 x==0임을 확인하는 코드이다. – Spin에서는 메시지 채널을 사용해 프로세스 사이에 통신한다. Spin은 다양한 타입의 메시지 채널을 제공한다. Buffered, non-buffered, 다양한 메시지 타입, 다양한 메시지 처리 연산

Tagged with: , , , , , , , , , ,
Posted in 1) Memo

20160531

동시성 프로그램의 이해 – SW coverage criteria에서 가장 강력한 coverage인 complete value coverage(CVC)를 테스팅하는 것이 model checking 기법이다. Model checking 기법은 각 변수의 모든 가능한 값을 대상으로 프로그램을 검증한다. 매우 많은 프로그램 상태가 발생하고, 따라서 작은 프로그램도 model checking하기는 쉽지

Tagged with: , , , , , , , , , , , , , , , , , , , ,
Posted in 1) Memo

20160526

동시성 프로그램의 이해 2) Testing Concurrent Programs to Achieve High Synchronization Coverage – Testing framework는 높은 coverage를 빠르게 달성하는 것이 중요하다. – Synchronization pair는 lock pair에 대한 coverage를 측정한다. 같은 thread라 하더라도 lock pair를 만들 수 있음. – Thread scheduling을

Tagged with: , , , , , , , , ,
Posted in 1) Memo
누적 방문자 수
  • 101,726 hits