안무 프로그래밍
Choreographic programming프로그래밍 패러다임 |
---|
컴퓨터 과학에서 안무 프로그래밍은 프로그램이 여러 동시 [1][2]참가자 간의 상호작용을 구성하는 프로그래밍 패러다임입니다.
개요
안무
안무 프로그래밍에서 개발자는 안무 프로그래밍 언어를 사용하여 동시 참가자의 의도된 커뮤니케이션 동작을 정의합니다.이 패러다임의 프로그램은 [1]안무라고 불립니다.안무 언어는 보안 프로토콜 표기법("앨리스 및 밥" 표기법이라고도 함)에서 영감을 얻습니다.이 언어들의 열쇠는 커뮤니케이션 프리미티브입니다. 예를 들어,
Alice.expr -> Bob.x
읽다Alice
표현 평가 결과를 전달하다expr
로.Bob
로컬 변수에 저장합니다.x
".[2] Alice, Bob 등은 일반적으로 역할 또는 [1]프로세스라고 불립니다.
다음 예시는 3가지 역할을 수반하는 Central Authentication Service(CAS; 중앙인증서비스)에 기초한 Simplified Single Sign-On(SSO; 단순 싱글사인온) 프로토콜의 안무를 보여 줍니다.
Client
액세스 토큰을 취득하려고 합니다.CAS
교감하다Service
.Service
(이것을 알아야 합니다)CAS
만약Client
접근권이 주어져야 합니다.CAS
이 서비스는 중앙인증서비스로,Client
의 자격 정보입니다.
안무는 다음과 같습니다.
클라이언트(credentials, 서비스)ID) -> CAS.authRequestCAS.check(authRequest)의 경우CAS.token = genToken(authRequest)CAS.Success(토큰) -> Client.resultCAS.Success(토큰) -> Service.result또 다른CAS.Failure -> Client.resultCAS.Failure -> Service.result
안무는 1라인부터 시작하는데요.Client
는, 몇개의 credential과 액세스 하고 싶은 서비스의 ID로 구성된 페어를 통신합니다.CAS
.CAS
로컬 변수에 이 쌍을 저장합니다.authRequest
(인증요구의 경우).회선 2에서는CAS
는 요구가 인증 토큰 취득에 유효한지 여부를 확인합니다.이 경우 토큰을 생성하여Success
토큰이 포함된 메시지Client
그리고.Service
(3 ~ 5행).그렇지 않으면CAS
인폼Client
그리고.Service
이 인증에 실패했을 경우,Failure
(7 ~ 8행)이 안무를 나머지는 SSO 안무라고 합니다.
끝점 투영
안무 프로그래밍의 주요 특징은 분산 구현에 대한 안무를 컴파일할 수 있다는 것입니다.이러한 구현은 [2][3]프로토콜에 따라 컴퓨터 네트워크에 참여해야 하는 소프트웨어 또는 독립 실행형 분산 프로그램을 [4][5]위한 라이브러리가 될 수 있습니다.
안무를 분산 프로그램으로 변환하는 것을 엔드포인트 투영(EPP)[1][2]이라고 합니다.
끝점 투영에서는 소스 [2]안무에 설명된 각 역할에 대한 프로그램이 반환됩니다.예를 들어, 위의 안무에 따라 엔드포인트 투영에서는 3개의 프로그램이 반환됩니다.하나는 다음 프로그램입니다.Client
, 1개:Service
, 및 용으로 1개CAS
이것들은 의사 코드 형식으로 다음에 나타냅니다.send
그리고.recv
는 다른 역할과 메시지를 송수신하기 위한 기본 요소입니다.
고객 | 서비스 | CAS |
---|---|---|
송신(크레덴셜, 서비스)ID)에서 CAS로CAS로부터의 recv 결과 | CAS로부터의 recv 결과 | 클라이언트로부터의 recv authRequest체크(authRequest)의 경우token = genToken(authRequest)클라이언트에 성공(토큰) 전송서비스에 성공(토큰) 전송또 다른클라이언트에 실패 전송서비스 장애 전송 |
각 역할에 대해 해당 코드는 다른 역할과 함께 안무를 올바르게 구현하기 위해 해당 역할이 수행해야 하는 작업을 포함합니다.
발전
안무프로그래밍의 패러다임은 명목상의 박사논문에서 [6][7][8]비롯되었다.안무 프로그래밍 언어의 구문에서 영감을 얻은 것은 "앨리스와 밥" 표기법으로도 알려진 보안 프로토콜 표기법에서 찾을 수 있습니다.안무 프로그래밍은 또한 프로세스 계산 [2][9]이론의 발전뿐만 아니라 서비스 안무와 상호작용 다이어그램의 표준에도 큰 영향을 받았습니다.
안무 프로그래밍은 활발한 연구 분야이다.이 패러다임은 정보 흐름,[10] 병렬 컴퓨팅,[11] 사이버-물리 시스템,[12][13] 런타임 적응 [5]및 시스템 [14]통합 연구에 사용되어 왔습니다.
언어들
- AIOCJ(웹사이트)[5]졸리에서 코드를 생성하는 적응 시스템을 위한 안무 프로그래밍 언어입니다.
- Chor(웹사이트).[4]세션 형식의 안무 프로그래밍 언어로 졸리의 마이크로 서비스로 컴파일합니다.
- 합창(웹사이트).Java 라이브러리로 컴파일하는 상위 객체 지향 안무 프로그래밍 언어입니다.
- 핵심 [15]안무안무 프로그래밍의 핵심 이론 모델입니다.구현은 Coq에서 [16][17]이용할 수 있습니다.
- 피루엣.[7]고차적 절차를 갖춘 기계화된 안무 프로그래밍 언어 이론입니다.
「 」를 참조해 주세요.
레퍼런스
- ^ a b c d Yoshida, Nobuko; Vasconcelos, Vasco T.; Padovani, Luca; Bono, Nicholas Ng; Neykova, Rumyana; Montesi, Fabrizio; Mascardi, Viviana; Martins, Francisco; Johnsen, Einar Broch; Hu, Raymond; Giachino, Elena; Gesbert, Nils; Gay, Simon J.; Deniélou, Pierre-Malo; Castagna, Giuseppe; Campos, Joana; Bravetti, Mario; Bono, Viviana; Ancona, Davide (2016). "Behavioral Types in Programming Languages". Foundations and Trends in Programming Languages. 3 (2–3): 95–230. doi:10.1561/2500000031.
- ^ a b c d e f Giallorenzo, Saverio; Montesi, Fabrizio; Peressotti, Marco; Richter, David; Salvaneschi, Guido; Weisenburger, Pascal (2021). Multiparty Languages: The Choreographic and Multitier Cases (Pearl). Leibniz International Proceedings in Informatics (LIPIcs). Vol. 194. pp. 22:1–22:27. doi:10.4230/LIPIcs.ECOOP.2021.22. ISBN 9783959771900. (ECoOP 2021 인정서)
- ^ 합창 프로그래밍 언어
- ^ a b Carbone, Marco; Montesi, Fabrizio (2013). "Deadlock-freedom-by-design". Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL '13. p. 263. doi:10.1145/2429069.2429101. ISBN 9781450318327. S2CID 15627190.
- ^ a b c Preda, Mila Dalla; Gabbrielli, Maurizio; Giallorenzo, Saverio; Lanese, Ivan; Mauro, Jacopo (2017). "Dynamic Choreographies: Theory and Implementation". Logical Methods in Computer Science. 13 (2). doi:10.23638/LMCS-13(2:1)2017. S2CID 5555662.
- ^ Montesi, Fabrizio (2013). Choreographic Programming (PDF) (PhD). IT University of Copenhagen. ISBN 978-87-7949-299-8. (EAPLS 최우수 박사학위 논문상)
- ^ a b Hirsch, Andrew K.; Garg, Deepak (16 January 2022). "Pirouette: higher-order typed functional choreographies". Proceedings of the ACM on Programming Languages. 6 (POPL): 1–27. doi:10.1145/3498684. (POPL 2022 인정어음)
- ^ Arend Rensink (2015-08-30). "Fabrizio Montesi wins the EAPLS Best PhD Dissertation Award 2014". European Association for Programming Languages and Systems.
- ^ Carbone, Marco; Honda, Kohei; Yoshida, Nobuko (2012). "Structured Communication-Centered Programming for Web Services". ACM Transactions on Programming Languages and Systems. 34 (2): 1–78. doi:10.1145/2220365.2220367. S2CID 15737118.
- ^ Lluch Lafuente, Alberto; Nielson, Flemming; Nielson, Hanne Riis (2015). "Discretionary Information Flow Control for Interaction-Oriented Specifications". Logic, Rewriting, and Concurrency (PDF). Lecture Notes in Computer Science. Vol. 9200. pp. 427–450. doi:10.1007/978-3-319-23165-5_20. ISBN 978-3-319-23164-8.
- ^ Cruz-Filipe, Luís; Montesi, Fabrizio (2016). "Choreographies in Practice". Formal Techniques for Distributed Objects, Components, and Systems. Lecture Notes in Computer Science. Vol. 9688. pp. 114–123. arXiv:1602.08863. doi:10.1007/978-3-319-39570-8_8. ISBN 978-3-319-39569-2. S2CID 18067252.
- ^ López, Hugo A.; Heussen, Kai (2017). "Choreographing cyber-physical distributed control systems for the energy sector". Proceedings of the Symposium on Applied Computing. pp. 437–443. doi:10.1145/3019612.3019656. ISBN 9781450344869. S2CID 39112346.
- ^ López, Hugo A.; Nielson, Flemming; Nielson, Hanne Riis (2016). "Enforcing Availability in Failure-Aware Communicating Systems". Formal Techniques for Distributed Objects, Components, and Systems. Lecture Notes in Computer Science. Vol. 9688. pp. 195–211. doi:10.1007/978-3-319-39570-8_13. ISBN 978-3-319-39569-2.
- ^ Giallorenzo, Saverio; Lanese, Ivan; Russo, Daniel (2018). "ChIP: A Choreographic Integration Process". On the Move to Meaningful Internet Systems. OTM 2018 Conferences (PDF). Lecture Notes in Computer Science. Vol. 11230. pp. 22–40. doi:10.1007/978-3-030-02671-4_2. ISBN 978-3-030-02670-7.
- ^ Cruz-Filipe, Luís; Montesi, Fabrizio (2020). "A core model for choreographic programming". Theoretical Computer Science. 802: 38–66. doi:10.1016/j.tcs.2019.07.005. S2CID 199122777.
- ^ Cohen, Liron; Kaliszyk, Cezary (2021). Formalising a Turing-Complete Choreographic Language in Coq. Leibniz International Proceedings in Informatics (LIPIcs). Vol. 193. pp. 15:1–15:18. doi:10.4230/LIPIcs.ITP.2021.15. ISBN 9783959771887. S2CID 231802115.
- ^ Cruz-Filipe, Luís; Montesi, Fabrizio; Peressotti, Marco (2021), Cerone, Antonio; Ölveczky, Peter Csaba (eds.), "Certifying Choreography Compilation", Theoretical Aspects of Computing – ICTAC 2021, Cham: Springer International Publishing, vol. 12819, pp. 115–133, doi:10.1007/978-3-030-85315-0_8, ISBN 978-3-030-85314-3, retrieved 2022-03-07