AI 퍼스트 개발, 코딩 가드레일, 그리고 폐기 가능한 아키텍처를 탐구합니다.
대규모 언어 모델은 test oracle 발견을 위한 괜찮은 브레인스토밍 파트너이지만, 속성을 환각하고 도메인 제약을 놓칩니다. 거짓 테스트를 배포하지 않고 이들을 사용하는 방법을 설명합니다.
사전에 올바른 출력을 알 수 없는 함수를 테스트해야 합니다. 경로 최적화기. 감정 분류기. 물리 시뮬레이션. metamorphic testing에 대해 읽어봤습니다: 반드시 성립해야 하는 입력과 출력 사이의 relation을 찾고, 정확한 값 대신 그 relation을 테스트합니다.…
모든 metamorphic relation이 버그를 잡아내는 것은 아닙니다. 약한 relation은 거짓 자신감을 주고, 강한 relation만이 실제 결함을 찾습니다. 차이를 구분하고 실제로 작동하는 relation 집합을 구축하는 방법을 설명합니다.
가격 책정 엔진에 대해 12개의 metamorphic relation을 작성했습니다. 모든 테스트가 통과합니다. 커버리지에 대해 기분이 좋습니다. 그런 다음 고객이 대량 할인이 거꾸로 계산된다고 보고합니다. relation 스위트를 확인합니다. 단 하나의 테스트도 실패하지 않았습니다.…
metamorphic testing은 정확한 예상 출력을 알지 못해도 코드의 정확성을 검증할 수 있게 해줍니다. 작동 방식, 한계, 그리고 시작하는 방법을 설명합니다.
고객 지원 티켓에 라벨을 붙이는 머신러닝 모델을 배포했습니다. 테스트 스위트는 초록색입니다. 모든 테스트가 통과했습니다. 그 테스트들 중 어느 것도 라벨이 올바른지 실제로 검사하지 않습니다. 올바른 라벨이 무엇인지 모릅니다. 아무도 모릅니다. 실제 입력에 대해 '올바른' 출력은…
phantom type과 `this` 파라미터를 사용하여 잘못된 protocol 전이를 런타임 버그 대신 컴파일 타임 오류로 바꾸는 방법.
모든 API 클라이언트 안에는 숨겨진 스테이트 머신이 있습니다. 먼저 handshake. 다음으로 인증. 세 번째로 데이터 전송. 마지막으로 종료. 그 순서를 어기면 런타임 오류, 혼란에 빠진 서버, 또는 더 나쁘게는 조용한 데이터 손상이 발생합니다. 대부분의 팀은 이러한 규칙을…
OpenAPI spec은 요청과 응답 schema를 기술하지만, 유효한 메시지 순서는 명시하지 않습니다. 여기서 OpenAPI가 줄 수 있는 것을 추출하는 방법과 여전히 직접 채워야 할 공백이 있는 부분을 설명합니다.
OpenAPI spec은 유효한 요청이 어떤 모습인지, 유효한 응답이 어떤 모습인지 알려줍니다. 하지만 를 이전에 호출할 수 있는지, 이후에 를 호출하면 어떤 일이 일어나는지는 알려주지 않습니다. 그 정보는 protocol spec에 있으며, OpenAPI는 protocol spec이…
세션 타입은 통신 프로토콜을 타입 시스템에 인코딩하여 런타임 프로토콜 오류를 컴파일 시간 오류로 변환한다. 프로덕션 코드가 사용할 수 있게 되기까지 연구 논문에서 30년을 보낸 이유는 다음과 같다.
세션 타입은 1993년에 발명되었다. 30년 후, 대부분의 네트워크 서비스는 여전히 프로토콜 상태를 수작업으로 작성한 런타임 검사로 검증하고 있다. 애초에 검증하는지조차 미지수다. 타입 시스템은 클라이언트가 전에 을 보냈는지, 또는 누군가 닫는 것을 잊어 연결이 누출되었는지에 대해…
세션 타입은 통신 프로토콜을 타입 시스템에 인코딩하여 코드가 실행되기 전에 메시지 전달 불일치를 컴파일러 오류로 변환한다.
데드락은 실행 시간 문제여야 한다. 그것이 데드락을 짜증나게 만드는 이유다. 코드는 깨끗이 컴파일되고, 테스트는 통과하며, 그런 다음 프로덕션에서 프로세스 A가 프로세스 B를 기다리고 프로세스 B가 프로세스 A를 기다리면서 멈춰 버린다. 세션 타입은 이를 뒤집는다. 프로세스 간 통신…
Infer를 사용하여 CI 파이프라인에서 형식적 정적 분석을 실행하는 방법. 작동하는 설정과 현실적인 트레이드오프를 소개한다.
abstract interpretation은 엔지니어가 탭을 닫게 만드는 유형의 용어다. 이해하려면 격자 이론을 한 학기 배워야 할 것처럼 들린다. 대부분의 개발자는 이것이 연구 논문에나 나오는 것이지 풀 리퀘스트에는 관련 없는 것으로 생각한다. 그 가정은 비싼 대가를 치른다.…
대규모 언어 모델은 정적 분석의 false positive을 선별하는 데 도움이 되지만, abstract interpretation처럼 프로그램의 의미론을 이해하는 것은 아니다. 두 가지를 결합하는 방법을 설명한다.
당신의 정적 분석기가 금요일 오후에 847개의 경고를 출력했다. 통계적으로 그중 5%에서 15%가 실제 버그다. 나머지는 false positive이다: 생성된 코드의 데드 스토어, 도구에게는 의심스러워 보이지만 사람에게는 분명한 널 체크, 중요하지 않은 해시 함수의 정수 오버플로.…
Facebook이 어떻게 abstract interpretation과 의도적인 unsoundness를 사용하여 수백만 줄의 Android 코드에서 race condition을 대규모로 발견했는가.
Facebook의 Android 앱에는 성능 문제가 있었다. UI 스레드가 작업에 압도당했지만, 코드를 백그라운드 스레드로 이동하면 race condition이 발생했다. 프로덕션의 크래시. 화난 사용자. 그들은 더 나은 코드 리뷰나 더 많은 테스트로 이를 해결하지 않았다. 그들은…