seunggi dfdgsdfg

ARM GPU 드라이브 버그부터 플러터 임펠러 엔진 수정까지

6월 배포 버전부터 프로덕션 앱의 크래시율이 급격히 올라갔다. 처음에는 미루고 미루었던 Flutter의 새 렌더러인 Impeller의 도입을 의심했다. 문제가 생긴 기기를 Skia로 되돌리자 크래시가 줄었지만, 그것으로 끝나지 않았다. 다른 모델에서 같은 문제가 발견됐고, 렌더러를 바꿔도 설명되지 않는 네이티브 크래시가 남았다.

스택을 하나씩 복원하며 추적한 끝에, 서로 다른 세 가지 문제를 찾았다. ARM GPU 드라이버의 텍스처 처리 버그, SQLite connection pool의 동시성 버그, Datadog의 JNI 객체 수명 문제였다.

두 건은 Flutter·ARM과 Datadog에 직접 신고했다. 특히 GPU 문제는 재현 앱을 만들고 Firebase Test Lab의 실기기에서 검증한 뒤, ARM의 버그 확인을 받아 Flutter Impeller 엔진 수정 PR이 머지되는 데까지 이어졌다. SQLite와 Datadog의 수정도 함께 적용하면서 프로덕션 크래시율을 크게 낮출 수 있었다.

먼저 사용자가 겪는 크래시부터 줄이기

수학자에게 Lean이 있다면 개발자에게는 TLA+가 있다

최근 OpenAI가 나비에–스토크스 문제의 해법과 Lean 형식화 증명을 공개했습니다. 아직 발표와 수학계의 최종 검증은 구분해야 하지만, 이번 소식에서 눈길이 가는 것은 AI가 만든 증명을 별도의 형식 시스템으로 검사한다는 점입니다. [^1]

Lean은 어떤 명제가 참인지, 혹은 거짓인지에 대한 증명을 기계적으로 확인하도록 도와주는 언어입니다. 그 바탕에는 개발자에게 익숙한 질문이 있습니다. “이 값은 이 타입에 속하는가?”[^2]

"이 값은 타입에 속하는가?" 를 살피는 행위자체가 수학적 증명입니다. 명제를 타입으로, 증명을 그 타입의 값으로 표현하는 대응, 이른바 커리–하워드 대응이 있습니다. Lean에서 p : P는 “값 p의 타입은 P다”라는 뜻인 동시에, P가 명제라면 “p는 명제 P의 증명이다”라는 뜻입니다. [^2]

수학: “명제 P의 증명 p가 있다. 따라서 P가 성립한다.”

저도 잘쪼개고, 잘 붙이기 위해 노력합니다. 대충 이런식이네요

점과 선으로 그래프 구조의 논리식을 세운다
- 이 때 그래프는 프로그램이 자신을 참조하거나 입력으로 받는 람다식의 특성상 순환구조가 나타나게 된다
- 이 때 그래프의 어떤 부분은 유향 비순환이고, 이것들은 대부분 쉽게 검증할수 있다. 그렇기에 이 것들을 최대한 끼고 살아야 한다
클린아키텍쳐, 의존성 역전, 구상보다는 추상에 의존하기 등등 수단과 방법을 가리지않고 부분을 유향비순환으로 격리, 즉 "잘 쪼개고"를 한다
- 이때 큰 구조는 최대한 단방향 의존성을 만들어 최대한 순환참조를 배제한다. 루프는 최대한 부분구조에 둔다
- 하지만 화면에 그림을 그리는 컴퓨터 구조는 기본적으로 이미 루프이다. 계속해서 화면을 뿌리는동안 사용자 입력을 중간중간 끼워넣고 컴퓨테이션 하는 식이다. e.g. 게임 루프
- 마찮가지로 동시성을 흉내내기위한 시분할이라던지, 비동기 연산등 컴퓨터, OS, 프로그래밍 언어 런타임등도 이벤트 루프등 루프를 활용한다
이렇게 제공되는 환경은 어쩔 수 없으니 그 외에 순환구조를 해야만 한다면, 자료구조 자체를 불변구조로 사용해서 최대한 정보를 가역적으로 유지한다. 정보에 대한 컴퓨테이션이 특히 루프에서 비가역적일경우 디버깅은 지옥으로 빠진다. react.js, flutter, swift ui 등 많은 현대 ui 라이브러리에서 이런 방식이 사용된다

이제 우리는 타입에 값을 넣는 행위 자체가 증명임을 알게됬다
- 수학자는 연역적으로 명제를 다루지만, 개발자는 요구사항을 구성하여 증명한다
여전히 수학에서 증명과 프로그래밍이 증명이라는 관점 사이에 여전히 거리감을 느낀다
- 이를테면, 내 상상속에 수학 증명은 모든 x 에 대해 보장한다. 모든 짝수x는 2로 나누어 떨어진다
하지만, 프로그래밍이, 내가 만든 어떤 논리식을 0과 1로 환원된 컴퓨테이션을 통해 증명하여, 런타임에서 죽지않는것을 보장하는 일이라면, 왜 어떤 입력 x에 대해서만 보장받고, 모든 입력 x에 대해서는 보장 받을수 없을까?
- 단순한 유닛테스트의 경우 어떤 x를 논리식에 직접 대입하여 증명한다. 어떤 x가 모든 x임을 보장할수 있는가?
int, float, double 은 32bit, 64bit 의 한계에 묶여있다. 이것 자체가 모든 R, Z, N 집합에 보장되는 연산을 할 수 없다
- float, double이 유한 개의 2의 거듭제곱 분모 집합으로 R을 모사하는 방식이기에 이 비유는 애초에 잘못된것이긴 하지만, 넘어가자
우리는 타입과 컴파일러를 통해 특정 지역공간에서 모든 x를 보장받는다
그리고-곱타입(class, struct, tuple), 또는-합타입(enum, sealed, union) 을 만들어서 단일 개체에 대한 참/거짓, 정합을 컴파일러의 도움을 받는다

JS에 커링이 과연 얼마나 잘어울리냐하는 흥미로운 논의가 꽤 있었는데요,

대표적으로 포문을 연 Brian Lonsdorf 의 Hey Underscore, You're Doing It Wrong! 이 있죠. https://www.youtube.com/watch?v=m3svKOdZijA https://www.slideshare.net/drboolean/underscore-18211797

사실 로다쉬나 언더스코어/백본을 통해 막 함수형의 장점이 아카데믹이 아닌 커뮤니티에도 받아들여지고 있었는데 이때부터 커링이라든지, 람다JS나 Fantasy Land등 나름 함수형 고급 주제들이 실 개발자에게도 받아들이기 시작된거 같아요

아무튼, 실질적으로 좀더 살펴볼 거는 알렉스의 Currying is not idiomatic in JavaScript 인데, 커링의 대안으로 어차피 커링이 파셜 애플리케이션에서 쓸거니 bind(null, target)과 같이 bind를 응용하거나 bind(null, target)의 신타스틱 슈거를 만드는 방안등이 논의되긴 했지요. http://2ality.com/2017/11/currying-in-js.html

https://news.ycombinator.com/item?id=18838115

	// This code is distributed under the MIT License.
	// Copyright (c) 2019 Remi Rousselet.
	// You can find the original at https://github.com/rrousselGit/provider.

	import 'package:flutter/material.dart';
	import 'package:google_fonts/google_fonts.dart';

	// This is a reimplementation of the default Flutter application
	// using provider + [ChangeNotifier].
	void main() {

	### Keybase proof

	I hereby claim:

	* I am dfdgsdfg on github.
	* I am dididi (https://keybase.io/dididi) on keybase.
	* I have a public key whose fingerprint is D0D3 959B 60B8 5953 605A 0EED 3B6E FDE9 1892 F7E4

	To claim this, I am signing this object:

	#!/usr/bin/env bash

	echo "=========================="
	echo "YOU NEED TO INSTALL PANDOC"
	echo "=========================="

	SRC_DIR='./src'
	DIST_DIR='./dist'
	files=($(find ${SRC_DIR} -type f -name '*.md'))