Alloy와 데이터베이스 동시 모험
이 글은 Alloy 모델링 언어를 사용하여 소프트웨어 개발을 지원하는 간단한 사례 연구이다.
소프트웨어 품질과 도구를 논하다
Typeable에서 우리는 소프트웨어의 질을 매우 중시하고 이 목표를 실현하기 위해 최선을 다할 준비를 하고 있다.우리가 현재 잘못된 접점을 없애는 것은 다음과 같다.
(Octopod, 다중 배포를 위한 오픈 소스 솔루션 보기)
이런 원가를 낮추는 방법의 하나는 가능한 한 빨리 오류를 발견하는 것이다.대략적으로 예측해 보면, 만약 형식 시스템이 당신의 오류를 포착한다면, 그것은 파일을 저장한 후 30초 안에 포착될 것이다.CI가 오류를 포착한 경우 오류 메시지를 생성하는 데 최대 30분이 소요됩니다.오류를 복구한 후 CI를 다시 실행하려면 30분을 더 기다려야 합니다.
멀리 갈수록 멈추는 시간이 길어지고 실수로 소모되는 자원도 많아진다. QA 단계에 도달하는 데 며칠이 걸릴 수도 있다. 그리고 QA 엔지니어가 당신의 일에 참여해야 한다.여기서 오류가 발견되면 QA는 오류 복구 후 다시 테스트를 해야 할 뿐만 아니라 개발자는 앞의 모든 단계를 다시 통과해야 합니다!
그렇다면 우리가 얼마나 멀리 가야 잘못을 빨리 발견할 수 있을까?놀랍게도 코드를 한 줄 작성하기 전까지는 우리가 오류를 포착할 수 있는 기회가 크게 높아질 수 있다!
합금에 들어가다
이것이 바로 합금의 용무의 땅이다.Alloy는 코드를 작성할 시스템에 테스트 가능한 사양을 구축할 수 있는 매우 간단하고 인체공학적인 모델링 도구입니다.
Alloy는 사용자의 생각이나 규범을 구축하는 데 사용되는 간단한 언어를 제공한다.Alloy는 모델이 완성될 때 사양이 허용하는 모든 불안한 사항을 보여주기 위해 최선을 다할 것입니다.이것은 또한 당신이 중요하게 생각하는 모든 속성에 대해 모델 검사를 할 수 있습니다.
예를 들자!최근에 우리는 다음과 같은 얄미운 문제에 부딪혔다.
newAuthCode
:: (MonadWhatever m)
=> DB.Client
-> DB.SessionId
-> m DB.AuthorizationCode
newAuthCode clid sid = do
let codeData = mkAuthCodeFor clid sid
void $ DB.deleteAllCodes clid sid
void $ DB.insertAuthCode codeData
return code
그럴 리가요?
모델링
상술한 문제는 합금 문제에 좋은 예를 제공하였다.우리들은 하나의 모델을 세워서 이 문제를 해결해 봅시다.구체적인 문제 사례를 시뮬레이션하기 위해 우리는 보통
newAuthCode의 조작부터 Alloy의 생각까지 묘사한다.즉, 먼저 하나의 조작 모델을 구축한 다음에 하나의 데이터베이스 모델을 구축하고 데이터베이스의 행위를 조작과 연결시켜 이를 보충해야 한다.그러나 이런 상황에서 우리의 조작이 어떤 개념처럼 보일 수 있는지를 형식화하면 문제를 발견할 수 있다는 사실이 증명되었다.
우리의 코드 세션이 묘사하는 과정은 두 가지 재미있는 부분이 있다.그것은 어느 시점에서 삭제된 다음 다른 시간에 새 영패를 삽입합니다.다음은 이러한 동작을 설명하는 합금 모델입니다.
open util/time // Import premade Time objects
sig Operation // There are operations...
{ delete : Time // ...that do a delete on some time instance
, insert : Time // ...and an insert at some other time
}
{ lt[delete,insert] // The deletes happen before the inserts
lt[first,delete] // And, for technical reasons, nothing happens
// during the first time instance.
}
run {some Operation} for 4 // Show me a random instance with up to
// 4 Operations
Operations개를 포함하는 무작위 우주가 생성된다.계속하려면 Alloy을 다운로드하고 위의 코드 세션을 복사해서 붙여넣으십시오.그런 다음 실행 및 표시를 눌러 모델의 다음 뷰를 봅니다.
Alloy가 더 많은 모델을 보여 주려면 "다음"을 누르십시오.
다음은 관계식 테이블로 나열된 인스턴스 중 하나입니다(다음을 몇 번 누른 다음 테이블 뷰를 선택해야 함).
┌──────────────┬──────┬──────┐
│this/Operation│delete│insert│
├──────────────┼──────┼──────┤
│Operation⁰ │Time¹ │Time³ │ ← Operation⁰ does a delete at Time¹ and
├──────────────┼──────┼──────┤ insert at Time³
│Operation¹ │Time² │Time³ │ ← Operation¹ does a delete at Time² and
└──────────────┴──────┴──────┘ insert at Time³
↑
Oh dear!
우리의 처리 프로그램은 병렬 호출되어 작업 순서가 심각하게 중첩되었다. 두 가지 작업이 있는데, 모두 같은 시간에 삭제 작업을 하고, 그 다음에 모두 같은 시간에 삽입 작업을 한다.또한 이것은 읽기가 아니기 때문에postgresql 기본 격리 단계는 이런 상황을 막지 않습니다.
벌레 찾았어!
우리가 고칠게!
내가 이 문제를 처음 조사했을 때, 나는 기본적으로 그것을 위해 다음과 같은 복구 프로그램을 짰다.
code <- run $ do
handleJust constraintViolation
(launchPG $ selectCodeForSession clid scope sid
(launchPG . pgWithTransaction $ newAuthCode clid scope sid)
select을 만들어서 이 기존 코드를 되돌려줄 수 있다. 왜냐하면 그것은 1분을 넘지 않기 때문이다.지금 괜찮아요?
이제 복구를 위한 빠른 합금 모델을 구축하여 올바른지 확인합니다.
open util/time // Import Time
sig Token {} // There are objects called tokens
one sig DBState // There is a database with some tokens
{userToken : Token lone -> Time}
// There are one or zero tokens at any given time in the DB
// (because database constraints don't allow for more than one)
sig Operation {
delete : Time
, insert : Time
, select : Time // Our operations can now also do a select
}
{
lt[first,delete] // Nothing happens on first time instance for
// technical reasons
lt[delete,insert] // delete happens first
lte[insert,select] // insert can happen after, or at the same time
// as delete
no userToken.(insert.prev) // If the insert works (ie. table is
=> insert = select // empty when we try, we get the value
// at the time of the insert (ie. we have
// 'INSERT RETURNING' statement)
// Otherwise, we execute the exception handler and
// the select may happen a bit later.
}
DBState을 추가했습니다. 이 동작은 코드의 동작과 유사해야 합니다.즉, 만약 시계가 비어 있다면, 우리는 영패를 삽입할 때 그것을 선택하고, 시계가 가득 차면, 우리는 잠시 후에 이상 처리 프로그램에서 그것을 선택할 것이다.그리고 우리는 모델에서 재미있는 부분, 즉 지정된 조작과 데이터베이스 상태 간의 상호작용에 들어간다.다행히도, 우리의 모형에 있어서 이것은 상당히 간단하다.
fact Trace { // The trace fact describes how our system behaves
all t : Time - first | { // at all time steps, except the first:
some delete.t => no userToken.t // If there is a delete, the table is empty
some insert.t => some userToken.t // If there is an insert, table is not empty
no delete.t and no insert.t // If there are no inserts and no deletes,
=> userToken.t = userToken.(t.prev) // the table does not change
}
}
이 모델을 실행하면 많은 실례가 생성되지만, 이전과 달리, 그것들을 훑어보기만 하면 뚜렷한 오류를 발견할 수 없습니다.하지만 Alloy에게 몇 가지 사실을 확인해 달라고 할 수 있습니다.이 점은 약간의 사고가 필요하지만, 모든 선택이 작용한다면, 우리의 복구가 작용할 것 같다.
그것을 단언으로 삼고, Alloy에게 그것이 성립되었는지 검사하도록 하자.
assert selectIsGood { // This is what we want Alloy to check
all s : Operation.select | // For all times when there is a select
some userToken.s // there is also a token in the database.
}
check selectIsGood for 6 // Check that selectIsGood is always true.
┌────────┬────────────┐
│DBState │userToken │
├────────┼──────┬─────┤
│DBState⁰│Token²│Time³│
│ │ ├─────┤ ← Token² is in the DB at Time³ and Time⁵
│ │ │Time⁵│
│ ├──────┼─────┤
│ │Token³│Time²│ ← Token³ is in the DB at Time².
└────────┴──────┴─────┘
↑
There are tokens in the table
only on Time², Time³ and Time⁵
Notably, there are no tokens at
Time⁴!
┌──────────────┬──────┬──────┬──────┐
│Operation │delete│insert│select│
├──────────────┼──────┼──────┼──────┤
│Operation⁰ │ TIME⁴│ Time⁵│ Time⁵│
├──────────────┼──────┼──────┼──────┤
│Operation¹ │ Time¹│ Time³│ TIME⁴│ ← The table is empty at Time⁴ and
├──────────────┼──────┼──────┼──────┤ the select fails for Operation¹!
│Operation² │ Time¹│ Time²│ Time²│
└──────────────┴──────┴──────┴──────┘
↑ ↑ ↑
These are the times when the
respective actions take place
따라서 유형 검사, 테스트, CI'd와 동업자 심사를 거친 건의는 사실상 잘못된 것이다!
병발성은 실현하기 어렵다.
내 배달
나는 위의 합금 모형을 쓰는 데 약 30분이 걸렸다.그에 비해 문제를 처음 이해하고 해결하는 데 걸리는 시간은 원래의 두 배가 될 수 있다.그리고 나도 30분을 기다렸다. CI를 기다렸다. 내 동료는 내 일을 되돌아보는 데 시간이 좀 걸렸다.
복구가 심지어 작용하지 않기 때문에, 나는 이 문제를 복구하는 데 걸리는 시간이 틀림없이 내가 문제를 발견했을 때 모델링을 멈추는 데 걸리는 시간보다 길다고 말할 수 있다.그러나 유감스럽게도 나는 합금을 전혀 건드리지 않았다. 왜냐하면 문제는 매우 간단하기 때문이다.
이런 공구를 사용하는 것이 가장 어려운 부분인 것 같다.언제 찾으러 오십니까?물론 모든 문제를 겨냥한 것은 아니지만, 지금보다 더 많이 할 수도 있다.
합금은 어디에서 살 수 있습니까?
만약 당신이 격노했다면, 여기에는 Alloy에 대한 링크가 몇 개 있습니다.
만약 당신이 격노했다면, 여기에는 Alloy에 대한 링크가 몇 개 있습니다.
https://alloytools.org/<- 여기서
https://alloy.readthedocs.io/en/latest/<- 이 서류들은 공식 서류
https://mitpress.mit.edu/books/software--abstractions-revised-edition<-합금에 관한 쉽게 읽을 수 있는 책이 책은 너에게 입문의 대부분 기본 모델을 제공할 것이다.
https://alloytools.org/citations/case-studies.html<-Alloy 작성자는 이 도구의 사용 목록을 저장합니다.그것은 매우 완전해서 각양각색의 용례가 있다.
Reference
이 문제에 관하여(Alloy와 데이터베이스 동시 모험), 우리는 이곳에서 더 많은 자료를 발견하고 링크를 클릭하여 보았다 https://dev.to/typeable/alloy-and-an-adventure-with-database-concurrency-4mg텍스트를 자유롭게 공유하거나 복사할 수 있습니다.하지만 이 문서의 URL은 참조 URL로 남겨 두십시오.
우수한 개발자 콘텐츠 발견에 전념
(Collection and Share based on the CC Protocol.)
좋은 웹페이지 즐겨찾기
