동시성 알고리즘에서 정확성의 중요성

동시성 분야의 전문가 페드로의 글을 하나 대략 번역하여 올립니다.

 

원문 https://concurrencyfreaks.blogspot.com/2021/12/the-importance-of-correctness-in.html

The importance of Correctness in concurrent algorithms

The importance of Correctness in concurrent algorithms

내 작업은 동시 알고리즘 영역에 있으므로 이 글은 이 분야에 대한 내 경험에 의해 크게 편향될 것입니다. 그렇긴 하지만, 내가 말하려는 대부분은 컴퓨터 과학의 다른 많은 분야와 다른 학문 분야에도 적용될 수 있다고 생각합니다.

나에게 Concurrent Algorithms 분야의 창작 과정은 Idea, The Algorithm, The Implementation의 세 가지 주요 단계로 구성됩니다.

The IDEA 

어떤 일을 시작하기 전에 아이디어가 필요합니다. 때때로 이것은 잘 형성된 아이디어이고, 다른 때는 우리가 이전에 아무도 하지 않은 방식으로 특정 문제를 해결하는 데 사용할 수 있다고 생각하는 통찰력이나 트릭 일 겁니다. 아마도 같은 문제를 더 빠르게 해결하거나 더 적은 메모리를 사용하여 해결하는 방법일 수 있습니다. 그것이 무엇이든, 그것은 당신에게 어떻게 든 이점을 제공합니다.

 

대부분의 사람들은 아이디어를 가질 수는 있지만 대부분의 아이디어는 이미 발견되었거나 틀렸거나 중요한 세부 사항에 대한 이해가 부족하기 때문에 쓸모가 없습니다. 후자는 내 경험에 비추어 보면 흔한 케이스 입니다. 

한 분야의 초보자는 일반적으로 이 범주에 속하는 아이디어를 가지고 있습니다. 단순하고 잘 알려진 개념 또는 다른 분야의 개념을 기반으로 하며, 이 분야의 기본(동시성)에 대한 지식과 당면한 문제에 대한 지식에 대한 이해가 부족합니다. 이러한 아이디어는 실제로 작동하지 않지만 초심자에게는 좋은 것처럼 보입니다.

한편으로는 괜찮은 생각을 가진 사람들의 그룹(클래스)이 있습니다. 일단 그들이 아이디어가 떠오르면, 이는 그들에게 소중하기도 하며 더 나은 것을 생각해내지 못할 가능성이 높기 때문에 이 아이디어에 매우 집착할 수 있습니다. 이것이 그들이 생각해낼 수 있는 최선이기 때문에 갓 구운 빵을 내보이는 것처럼 서둘러 정리하려고 할 것 입니다.

당신은 그들이 거기에 도달하기 위해 열심히 일했다는 것을 이해해야 합니다. 따라서 그들이 이 아이디어를 가치 있게 여기고 필요하다면 손톱과 이빨로 그것을 지키기 위해 싸우고 싶어하는 것은 지극히 정상입니다. (안타깝게도) 이러한 부류의 사람들은 함께 추론하며 문제를 해결할 더 나은 방법을 있다고 알려주는 것은 매우 어려울 수 있습니다. 

이 범주의 사람들은 초보자가 아닙니다. 그들은 일반적으로 해당 분야에 대한 지식을 어느 정도 가지고 있습니다. 때때로 그들은 오랫동안 현장에서 일했기 때문에 스스로를 전문가라고 부릅니다.

아이디어가 많은 사람들의 세 번째 그룹이 있습니다. 이 그룹에 가려면 아이디어를 내는 데 능숙해야 할 뿐만 아니라 특정 분야에 대한 많은 지식이 있어야 하기 때문에 이들은 소규모 그룹으로 구성됩니다. 내 추측에 따르면 한 분야에 대해 깊이 있게 배우는 데 필요한 사고 방식은 한 분야에서 혁신하는 데 필요한 사고 방식과 거의 반대입니다. 앞의 사고방식은 이전에 이 분야에서 다른 사람들이 수행한 많은 것을 기억하고 수용해야 하는 사고 방식인 반면, 혁신의 사고 방식은 우리에게 배우는 모든 것에 대해 질문하는 것입니다.

분명히 두 가지 사고 방식이 상호 배타적인 것은 아니지만 특정 분야의 연구원 중 소수만이 두 가지 사고 방식을 모두 가지고 있다고 가정해 보겠습니다. 이 세 번째 그룹의 주요 특징은 아이디어가 많다는 것입니다. 이러한 아이디어의 대부분은 등급이 낮고, 몇 개는 괜찮은 편이며, 때때로 하나의 아이디어는 훌륭할 것입니다. 그들은 아이디어가 많기 때문에 이 그룹의 연구원들은 자신의 아이디어에 집착하지 않습니다. 그들은 다른 아이디어가 (자신이나 다른 연구자에게) 올 것이고 그 아이디어가 약간 더 나은 균형을 갖고 약간 다른 측정 기준에서 더 나을 것이라는 것을 알고 있습니다. 그들은 완벽한 솔루션은 없으며 완벽의 개념은 당면한 문제의 특수성에 달려 있음을 이해합니다.

 
The Algorithm

아이디어가 생기면 다음 단계는 그것을 알고리즘으로 변환하는 것입니다. 많은 사람들이 아이디어와 알고리즘을 혼동합니다. 그것들은 같은 것이 아닙니다. 아이디어는 문제에 대한 가능한 솔루션에 대한 모호한 설명으로, 여러 부분이 함께 작동하는 방식이나 그 배후의 주요 트릭이 무엇인지 강조합니다. 아이디어는 엘리베이터 피치 또는 화이트보드의 그림으로 생각할 수 있습니다. 알고리즘은 이 솔루션에서 취한 단계에 대한 정확한 설명입니다. 그것은 우리가 문제를 해결하거나 계산을 실행하는 방법에 대한 의사 설명이며 프로그램에 대한 설명입니다. 프로그래밍 언어로 작성할 필요는 없으며 단계는 영어로 작성할 수 있지만 설명적이어야 합니다.

내 경험에 따르면, 아이디어와 알고리즘의 이러한 혼동은 초보자 수준에서 많은 마찰을 일으킵니다. 초보자는 이 두 개념의 차이점을 이해하는 데 어려움을 겪습니다. 그들에게 아이디어는 구현으로 이동하기에 충분합니다. 누락된 부분이 있는 경우 구현 중에 찾아내고 구현 세부 정보로 남겨둡니다. Idea와 Algorithm은 모두 영어로 설명할 수 있지만 구현은 소스 코드(즉, 프로그래밍 언어)로 설명되어 있다는 사실은 초보자에게 아이디어와 알고리즘의 구분을 더욱 어렵게 만듭니다.
 
아마도 이것을 생각하는 가장 좋은 방법은 수학의 맥락에 두는 것입니다. 이론 수학 분야에는 "구현 단계"가 없고 아이디어와 알고리즘만 있습니다. 그러나 수학자에게는 아이디어와 알고리즘 사이에 분명한 차이가 있습니다. 알고리즘은 정확(또는 부정확)한 것으로 입증될 수 있지만 아이디어는 입증할 수 없습니다(분명히 틀리지 않는 한). 아이디어는 영어로 설명하고 알고리즘은 수학 표기법으로 설명하는 데 도움이 됩니다. 또한 알고리즘을 지원하기 위한 형식적 증명이 있다는 것도 도움이 되지만 이에 대한 자세한 내용은 포스트 후반부에 있습니다.
 
이 수학적 사고 방식은 동시 알고리즘에 대한 연구에 많은 도움이 됩니다. 아이디어를 설명할 때 나는 엘리베이터 피치를 하거나 화이트보드에 그림을 그리거나 몇 가지 파워포인트 애니메이션을 만듭니다. 알고리즘을 설명할 때 의사 코드를 사용하거나 영어 문장을 사용하는 경우 각 단계를 항목화하고 최대한 설명하려고 합니다.

완벽하지는 않지만 두 단계를 구분하는 데 도움이 됩니다.
 

The Implementation

동시성 알고리즘 분야에서는 일반적으로 알고리즘을 구현합니다. 구현은 프로그래밍 언어로 이루어집니다. 목표가 연구 논문이라면 언어는 이 작업을 수행하는 연구원들이 편안하게 사용할 수 있는 것이면 무엇이든 될 수 있습니다. 목표가 회사의 실제 문제를 해결하는 것이라면 특정 문제 또는 이 기능을 지원하는 그룹이 수행해야 하는 프로그래밍 언어/도구에 따라 언어가 결정됩니다.

구현을 하는 이유는 무엇입니까?
첫째, 우리가 할 수 있기 때문입니다.
둘째, 구현을 하면 개념-증명(POC) 구현이더라도 솔루션의 성능을 이해하는 데 도움이 되기 때문입니다.
셋째, 업계에서는 구현이 궁극적으로 필요한 것이기 때문이고 이는 실제로도 해결하려는 문제를 실제로 해결하는 방법이기 때문입니다.
넷째, 구현을 테스트할 수 있고 이러한 테스트를 통과하면 알고리즘이 정확하다는 확신을 갖는 데 도움이 됩니다. 다음 섹션에서 이에 대해 자세히 설명합니다.

How do we know it's correct?

새로운 알고리즘을 설계하거나 읽을 때 우리는 항상 그것이 맞는지 아닌지 궁금해 합니다. 이 문제를 해결하는 두 가지 방법이 있습니다. 형식적 증명(formal verification)과 스트레스 테스트입니다. 가장 좋은 방법은 두 가지를 모두 수행하는 것이지만 이것이 항상 가능하거나 유용한 시간 투자는 아닙니다. 학계에서는 새로운 동시성 알고리즘에 대한 연구 논문을 작성할 때 형식적인 증명이 선호되는 접근 방식입니다. 작은 경우에는 종이 자체에 증거물을 넣을 수 있고, 그렇지 않으면 첨부 문서나 부록에 넣을 수 있습니다.

 

일부 이론 학회와 저널은 알고리즘 구현에 신경조차 쓰지 않습니다. 그들이 걱정하는 것은 증명이 잘 구성되어 있고 증명하려는 내용을 실제로 증명하는지 여부입니다.

 

보다 실용적인 학회(동시성 분야에서)는 일반적으로 스트레스 테스트에 대해서도 별로 신경 쓰지 않습니다. 그들은 구현이 이루어졌다는 사실과 이 구현으로 만들어진 벤치마크를 중요시하지만 구현의 정확성을 테스트하는 지원 코드는 중요하지 않습니다. 그리고 리뷰어들이 이것을 중요하게 여기지 않기 때문에 논문을 제출하는 연구원들도 테스트를 하는 데 시간을 할애하지 않습니다. 이 분야에서 일하는 나의 동료 중 한 사람만이 유일하게 자신의 업무에 대한 스트레스 테스트를 작성하는 데 지속적으로 시간을 할애합니다.

대부분의 동료 연구 동료들은 자신의 작업에 대해 스트레스 테스트를 하지 않고 대신 공식적 정확성 증명을 작성하는 데 시간을 할애하는 것을 선호합니다. 인센티브가 없을 뿐입니다.

연구 논문을 작성하는 데는 시간이 걸립니다. 논문의 가치가 있는 아이디어를 내는데 시간이 걸리고, 알고리즘으로 전환하는 데 시간이 걸리고, 구현하는 데 시간이 걸리고, 벤치마킹하는 데 시간이 걸리고, 리뷰어를 기쁘게 하는 방식으로 그것에 대해 작성하는 데 시간이 걸립니다. 그리고 그 위에 스트레스 테스트를 작성해야 한다면 할 일이 너무 많습니다. 증명은 인간, 일반적으로 올바른 것으로 입증된 알고리즘을 설계한 동일한 인간에 의해 이루어지므로 알고리즘에서 오류를 유발한 동일한 오류가 증명에 침투할 수 있습니다. 이것은 증명의 종류에 따라 다릅니다. 예를 들어, 불변 증명이 이 악의적인 효과에 덜 취약하다고 주장할 수 있지만 그것에 면역될 방법은 없습니다.
 
소프트웨어 산업계에서는 사고 방식이 거의 반대입니다. 여기서 우리는 각 증명이 알고리즘 및 구현과 밀접하게 연관되어 있기 때문에 형식 증명에 대해서는 신경 쓰지 않습니다. 한 줄의 코드를 변경하면 해당 증명이 무효화될 수 있습니다. 이것은 잠금이 없는 알고리즘에서 특히 사실이지만 일반적으로 동시성 알고리즘에 대한 일반적인 설명입니다. 비즈니스 요구 사항이 변경될 수 있습니다. 즉, 코드에 새로운 기능이 포함될 수 있습니다. 즉, 시간이 지남에 따라 구현이 변경됩니다. 누군가가 한 줄의 코드를 변경할 때마다 새로운 증명을 작성하는 것은 실용적이지 않습니다.

네 물론 TLA+와 같은 도구가 있지만 증명과 구현을 동기화 상태로 유지해야 합니다. 반면에 구현을 다루기 위해 테스트를 작성하면 코드 줄을 변경할 때마다 테스트를 다시 실행할 수 있습니다. 아무것도 깨지지 않았다는 100% 보장을 제공하지는 않지만 많은 실수를 잡는 데 도움이 될 것입니다. 또한 업계에서는 실제로 작동하는 구현을 원합니다. 이 알고리즘의 구현이 버그로 가득 차 있다면 올바른 것으로 입증된 알고리즘이 무슨 소용이 있습니까?

엔지니어에게 공식 증명이나 TLA+ 증명을 작성하게 하는 것보다 구현의 정확성을 주장하는 테스트를 하는 것이 엔지니어의 시간을 훨씬 더 잘 활용하는 것 입니다. 

Tests imply re-usability

나의 지능은 큰 동시성 알고리즘을 다루기에 버겁습니다. 그래서 나는 할 수 있는 다른 연구원을 알고 있으며 Andreia가 그 한 예입니다.  만약 당신이 나에게 큰 새로운 동시성 알고리즘을 제시한다면, 나는 내 머리 전체를 그 알고리즈믕로 채울 수 없을 것이기 때문에 옳고 그름을 스스로 확신하지 못할 수도 있습니다. 가능한 모든 단계의 인터리빙을 거치거나 그 정확성에 대해 추론할 수는 없습니다.

그것은 보드에서 7개의 움직임을 볼 수 있는 체스 선수와 3개의 움직임만 볼 수 있는 체스 선수와 같습니다. 네, 연습할 수 있는 기술이지만, 어느 정도 나이가 들면 머리에 딴 생각이 들게 되고, 솔직히 말해서 그런 큰 알고리즘을 파악하는 데 걸리는 시간을 투자하고 싶지도 않습니다. 이 때문에 나는 되도록 작은 알고리즘으로 나의 관심을 제한합니다. 물론 작은 알고리즘에 대해서도 스트레스 테스트를 합니다.

대기열의 동작을 다루는 테스트가 있는 경우 우리가 설계하고 구현하는 모든 새 대기열은 동일한 테스트로 테스트할 수 있습니다. 특정 대기열이 우리가 수년에 걸쳐 설계한 모든 테스트를 통과하면 이것이 올바른 대기열 구현이고 결과적으로 대기열의 알고리즘이 정확할 가능성이 높다는 확신을 갖게 됩니다. 게다가, 잘 테스트된 대기열을 갖는다는 것은 대기열이 필요한 다른 동시성 메커니즘을 설계할 때 우리가 디자인하는 새로운 것에서 문제를 발견할 때(필연적으로 그렇게 할 것입니다) 때문에 미리 디자인한 대기열을 사용할 수 있다는 것을 압니다. 우리는 이러한 문제가 대기열 자체의 문제로 인한 것이 아니라 대기열 상단에서 작동하는 알고리즘에서 발생한다는 것을 확신할 것입니다.

우리가 하는 모든 일에 스트레스 테스트를 하면 재사용성을 확보할 수 있습니다! 그리고 예, 스트레스 테스트는 구현이 정확하다는 100% 보장은 아니지만 확실히 아무것도 없는 것보다 낫습니다. 그리고 저는 주장할 것입니다. 증명도 능가합니다.  증명은 구현이 아니라 알고리즘에 대한 것입니다. 반면에 스트레스 테스트는 구현 및 알고리즘의 정확성을 검증합니다. 일타이피! 더 나은 시간 투자입니다.
  
구현을 재사용할 수 있을 뿐만 아니라 테스트를 다른 구현에서도 재사용할 수 있습니다. 동시 집합의 불변량을 확인하기 위해 스트레스 테스트를 설계할 때 동일한 테스트를 사용하여 다른 집합 구현의 정확성을 확인할 수 있습니다. 우리가 하는 테스트는 미래를 위한 투자가 되어 시간이 지남에 따라 그 혜택을 누리게 됩니다. 

My take on correctness

정확성에 대한 나의 견해

새로운 잠금이 없는 데이터 구조를 생각해 냈고 이제 이에 대한 내 도움을 원한다고 가정해 보겠습니다. 당신이 한 일이 옳았다고 확신할 수 있는 두 가지 다른 방법이 있습니다.

1.알고리즘과 함께 정확성을 형식 증명 합니다.
2.생각할 수 있는 만큼 스트레스/불변 테스트를 만들고 알고리즘 구현이 이러한 테스트를 통과하도록 합니다.
이상적으로는 둘 다 있어야 하지만 하나만 하려면 2번으로 가십시오.

둘 다에 알고리즘이 필요합니다. 알고리즘이 없으면 아무것도 없습니다. 어떤 사람들은 아이디어에서 구현 단계로 바로 넘어갑니다. 이것은 알고리즘이 머리 속에만 산다는 것을 의미합니다. 그들에게는 좋지만, 연구 논문의 요지는 정보를 공유하는 것이고, 다른 사람에게 구현에서 알고리즘을 리버스 엔지니어링하도록 강요하는 것은 좋은 공유 방법이 아닙니다. 그리고 아마도 아무도 그렇게 하려고 애쓰지 않을 것입니다.

예, 알고리즘이 없으면 큰 가치있는 것을 얻을 수 없습니다.
 

Summary

요약하면 스트레스/불변 테스트를 작성하는 이유는 다음과 같습니다.

- 이 테스트는 나중에 다시 사용할 수 있습니다.
- 알고리즘과 구현의 정확성을 증명하는 데 도움이 됩니다.
- 이러한 스트레스 테스트로 검증된 알고리즘은 더 복잡한 알고리즘의 빌딩 블록으로 사용될 수 있습니다.
- 테스트가 있는 경우 다른 연구자의 알고리즘을 검증할 수 있습니다.
- 알고리즘을 수정하면 처음부터 새로운 증거를 만들 필요 없이 수정된 알고리즘의 정확성을 다시 확인할 수 있습니다.
- 테스트 작성은 재미있습니다!