안무 프로그래밍

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는 다른 역할과 메시지를 송수신하기 위한 기본 요소입니다.

SSO 안무의 엔드포인트 투영(EPP)
고객 서비스 CAS
송신(크레덴셜, 서비스)ID)에서 CAS로CAS로부터의 recv 결과
CAS로부터의 recv 결과
클라이언트로부터의 recv authRequest체크(authRequest)의 경우token = genToken(authRequest)클라이언트에 성공(토큰) 전송서비스에 성공(토큰) 전송또 다른클라이언트에 실패 전송서비스 장애 전송

각 역할에 대해 해당 코드는 다른 역할과 함께 안무를 올바르게 구현하기 위해 해당 역할이 수행해야 하는 작업을 포함합니다.

발전

안무프로그래밍의 패러다임은 명목상의 박사논문에서 [6][7][8]비롯되었다.안무 프로그래밍 언어의 구문에서 영감을 얻은 것은 "앨리스와 밥" 표기법으로도 알려진 보안 프로토콜 표기법에서 찾을 수 있습니다.안무 프로그래밍은 또한 프로세스 계산 [2][9]이론의 발전뿐만 아니라 서비스 안무와 상호작용 다이어그램의 표준에도 큰 영향을 받았습니다.

안무 프로그래밍은 활발한 연구 분야이다.이 패러다임은 정보 흐름,[10] 병렬 컴퓨팅,[11] 사이버-물리 시스템,[12][13] 런타임 적응 [5]시스템 [14]통합 연구에 사용되어 왔습니다.

언어들


「 」를 참조해 주세요.

레퍼런스

  1. ^ 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.
  2. ^ 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 인정서)
  3. ^ 합창 프로그래밍 언어
  4. ^ 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.
  5. ^ 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.
  6. ^ Montesi, Fabrizio (2013). Choreographic Programming (PDF) (PhD). IT University of Copenhagen. ISBN 978-87-7949-299-8. (EAPLS 최우수 박사학위 논문상)
  7. ^ 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 인정어음)
  8. ^ Arend Rensink (2015-08-30). "Fabrizio Montesi wins the EAPLS Best PhD Dissertation Award 2014". European Association for Programming Languages and Systems.
  9. ^ 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.
  10. ^ 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.
  11. ^ 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.
  12. ^ 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.
  13. ^ 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.
  14. ^ 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.
  15. ^ 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.
  16. ^ 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.
  17. ^ 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

외부 링크