20160405

동시성 프로그램의 이해
– 버그에 대한 정의가 모호할 수 있다. 프로그램이 실행 중에 죽는 것은 확실히 버그이다. 프로그램이 죽지 않고 실행된다고 해서 버그가 없다고 할 수 있나? 프로그램에 버그가 있는지 아닌지의 여부는 요구사항에 따라 달라질 수 있다. 따라서 요구사항에 대한 정의가 중요하다.
– Concurrent program이 점점 더 많이 사용되고 있다. 하지만 Concurrent program은 버그 없이 코딩하기도 어렵고, 버그를 찾기도 어렵다. “Most of my subjects (interviewee) have found that the hardest bugs to track down are in concurrent code” (Coders at work 인용)
– 지금까지 만든 프로그램은 deterministic했을 것. 하지만 동시성 프로그램은 non-deterministic하다. Deterministic 프로그램은 입력에 대해 출력이 동일하다. Non-deterministic 프로그램은 입력에 대해 출력이 다를 수 있다. 따라서 concurrent program은 실행 시마다 버그가 발견될 수도, 발견되지 않을 수도 있다.
– Concurrent program의 올바름을 보장하기는 매우 어렵다. 쓰레드 사이의 상호작용을 모두 확인해야 하고, 이를 위해서는 지금까지 사용한 테스팅 기법이 아닌 새로운 것이 필요하다. 예를 들어 Peterson mutual exclusion의 가능한 모든 경우를 확인한다고 해보자. 두 개의 프로세스만 있다면 30개의 상태만 검증하면 되지만, 세 개의 프로세스라면 853개의 상태, 네 개의 프로세스라면 55043개의 상태를 검증해야 한다.
– 다음 코드에서 thread interleaving scenario의 수는 20개, unique outcome의 수는 11개. 실행 방식과 각 값 예측 기법들이 필요함. 동시성 프로그램에 대한 이해가 없으면 그 결과를 알 수가 없게 됨. 이같은 문제들을 사람이 분석하기는 힘들다. 알고리즘과 툴을 만들어서 해결해야 함.

void p() {x=y+1; y=z+1; z= x+1;}
void q() {y=z+1; z=x+1; x=y+1;}

– Mutual exclusion protocol에 오류가 있는 예제
an example of mutual exclusion protocol.PNG
– Model checking technique에는 multiple update, singular update가 있을 수 있는데, 일반적으로 singular update를 많이 사용한다. Model checking technique 관점에서 보았을 때, 소프트웨어는 execution tree로 볼 수 있다. Execution tree는 프로그램의 상태로 구성된 트리이며, 프로그램의 한 문장을 실행할 때마다 상태 전이가 발생한다.
operational semantics of software.PNG
– SW 테스팅에는 coverage가 있다. Edge coverage는 모든 branch를 테스팅하는 것. Edge coverage가 만족하면 node coverage도 만족한다. SW coverage hierarchy에서 더 높은 것이 더 강한 coverage이다. Complete value coverage는 모든 변수의 모든 범위에 대해 확인하는 것. Complete value coverage는 원래 어려웠는데, symbolic testing 기법을 적용하면 가능함. 현실적으로는 complete path coverage (concolic testing)을 많이 한다. 가능한 모든 경로
를 테스팅하는 것.
hierarchy of SW coverage criteria.PNG

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

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s

누적 방문자 수
  • 96,405 hits
%d bloggers like this: