Oturum Tipleri ve Tiplendirilmiş Eşzamanlılık
Oturum tipleri, bir kanal boyunca iletişimin protokolünü tanımlayan davranışsal tiplerdir ve tip kontrolünün eşzamanlı süreçlerin doğru şekilde etkileşim kurmasını garanti etmesini sağlamaktadır.
Tanım
Bir oturum tipi, bir iletişim kanalı tarafından takip edilen protokolü, gönderilen ve alınan mesajların sırasını ve tiplerini tanımlayan bir tiptir; böylece bir tip denetleyici, katılımcıların iyi tanımlanmış bir protokole göre iletişim kurmasını sağlayabilmektedir.
Kapsam
Bu konu, eşzamanlılık için tip disiplinlerini, özellikle iletişim kuran süreçler arasında değiş tokuş edilen mesajların sırasını ve şeklini belirten oturum tiplerini ve davranışsal tipleri kapsamaktadır. İkili ve çok taraflı oturum tiplerini, ikilik (duality) ve protokol uyumluluğunu, iletişim güvenliği ve kilitlenme (deadlock) özgürlüğü garantilerini ve oturum tipleri ile doğrusal mantık (linear logic) arasındaki yazışmayı içermektedir.
Temel sorular
- Bir tip, bir kanal üzerindeki iletişim protokolünü nasıl tanımlayabilir?
- İkilik (duality) nedir ve iki uç noktanın anlaşmasını nasıl sağlamaktadır?
- Tip kontrolü ile iletişim güvenliği ve kilitlenme özgürlüğü nasıl garanti edilmektedir?
- Curry-Howard yazışması aracılığıyla oturum tipleri doğrusal mantıkla nasıl ilişkilidir?
Temel kuramlar
- İkili oturum tipleri
- Honda, Vasconcelos ve Kubo, yapılandırılmış iletişim için oturum tiplerini ve bir ikilik disiplinini tanıtmış, bir kanalın iki uç noktasının tamamlayıcı, uyumlu protokolleri takip etmesini sağlamıştır.
- Çok taraflı oturum tipleri
- Honda, Yoshida ve Carbone, oturum tiplerini, yerel tiplere yansıtılan küresel bir protokol aracılığıyla birden fazla katılımcıya genelleştirerek birçok taraf arasında güvenli etkileşimi garanti etmiştir.
- Doğrusal önermeler olarak oturum tipleri
- Caires ve Pfenning, oturum tipleri ile sezgisel doğrusal mantık (intuitionistic linear logic) arasında bir Curry-Howard yazışması kurmuş, tiplendirilebilirlikten kilitlenme özgürlüğü gibi güçlü garantiler elde etmiştir.
Klinik önem
Oturum ve davranışsal tipler, eşzamanlı ve dağıtık yazılımlara protokol uyumluluğu, iletişim güvenliği ve kilitlenme özgürlüğü gibi statik garantiler getirmekte ve dil uzantılarına ve kütüphanelere entegre edilmiştir. Çalışma zamanında ortaya çıkabilecek protokol hatalarını derleme zamanı tip hatalarına dönüştürmektedirler.
Tarihçe
Oturum tipleri, tiplendirilmiş pi-calculus üzerine yapılan çalışmalardan ortaya çıkmış, 1993-1998 yıllarında Honda ve meslektaşları tarafından ikili oturumlar için resmileştirilmiştir. Çok taraflı oturum tipleri, 2008'de teoriyi birçok katılımcıya genişletmiş ve Caires ile Pfenning'in 2010'daki mantıksal yazışması, oturum tiplerini doğrusal mantıkla ilişkilendirerek kilitlenmesiz tiplendirilmiş eşzamanlılık araştırmalarını ve pratik araçları teşvik etmiştir.
Tartışmalar
- Davranışsal tiplendirmenin ifade gücü ve pratikliği
- Araştırmacılar, oturum tipi sistemlerinin ne kadar zengin olması gerektiğini tartışmakta, kilitlenme özgürlüğü ve protokol uyumluluğu gibi garantilerin gücünü, ana akım dillerdeki ek açıklama yükü ve entegrasyon zorluğu ile dengelemektedir.
Öne çıkan isimler
- Kohei Honda
- Nobuko Yoshida
- Marco Carbone
- Luís Caires
- Frank Pfenning
İlgili konular
Temel eserler
- honda1998
- honda2008
- caires2010
Sıkça sorulan sorular
- Bir oturum tipi neyi garanti eder?
- İyi tiplendirilmiş bir oturum, iletişim güvenliğini garanti eder; yani her mesaj beklenen tipe sahiptir ve taraflar üzerinde anlaşılan protokolü takip eder; daha zengin sistemler ayrıca ilerlemeyi veya kilitlenme özgürlüğünü garanti etmektedir.
- Oturum tiplerinde ikilik (duality) nedir?
- İkilik, bir kanalın iki uç noktası arasındaki ilişkidir: bir uç noktanın gönderdiği her şeyi diğerinin alması gerekir ve bunun tersi de geçerlidir, böylece iki yerel protokol tutarlı bir konuşma oluşturacak şekilde bir araya gelmektedir.