- TLA+, kod düzeyinde değil daha üst bir düzeyde yazılım modellemek ve devre düzeyinde değil daha üst bir düzeyde donanım modellemek için kullanılan bir dildir
- Model yazıp bunları inceleyebileceğiniz bir entegre geliştirme ortamı (IDE) sunar
- Mühendislerin en çok kullandığı araç TLC model denetleyicisidir; ayrıca bir ispat denetleyicisi de sunulur
- TLA+ matematik temellidir ve herhangi bir programlama diline benzemez
- Çoğu mühendis için TLA+'a doğrudan başlamak yerine PlusCal ile başlamak daha kolaydır
- TLA+ modelleri genellikle "specification" olarak adlandırılır. Aşağıdaki tanıtımda buna
model denir
PlusCal
- PlusCal, algoritma yazmak, özellikle de paralel ve dağıtık algoritmalar yazmak için kullanılan bir dildir
- Sözde kod yerine, algoritmaları test edilebilir ve kesin kodla yazmak için kullanılır
- Basit bir programlama dili gibi görünür ve eşzamanlılık ile belirlenimsizliği ifade edebilen yapılar sunar
- Matematiksel formüller ifade olarak kullanılabildiği için oldukça yüksek ifade gücüne sahiptir
- PlusCal algoritmaları TLA+ modeline dönüştürülür ve TLA+ araçlarıyla doğrulanabilir
- Programlama dili gibi göründüğü için öğrenmesi kolaydır, ancak karmaşık modelleri yapılandırmak için TLA+ daha uygundur
Model nedir
- Bilgisayarlar ve ağlar sürekli fizik yasalarına uyar, ancak bunların davranışını ayrık olaylar kümesi olarak modellemek doğaldır
- Gerçek bir sistemi kusursuz biçimde betimleyen model yoktur; model, sistemin belirli bir amaç için bazı yönlerini betimler
- TLA+, durum tabanlı bir modelleme dilidir ve bir sistemin çalışmasını durumlar dizisi olarak ifade eder
- Olaylar, art arda gelen iki durumun çiftiyle ifade edilir ve buna 'adım (step)' denir
- Sistem, olası tüm çalışmaları açıklayan eylemler kümesi olarak modellenir
Kod düzeyinin ötesinde modelleme
- TLA+, kod düzeyinin üzerindeki sistem modellemesinde kullanılır
- Örneğin, Öklid algoritması kod olarak değil, EBOB'u (GCD) hesaplayan bir prosedür olarak açıklanabilir
- x değişkeni M'ye, y değişkeni N'ye ayarlanır
- x ile y'den küçük olan değer, büyük olandan tekrar tekrar çıkarılır
- x ile y eşit olana kadar yineleme sürer ve bu değer GCD'dir
- Bu tür açıklamalar değişken türleri veya istisna işleme gibi ayrıntıları atlar ve yalnızca algoritmanın özünü ifade eder
- Yalnızca kodlamaya odaklanılırsa iyi algoritmalar bulmak zorlaşır → soyut düşünme gerekir
- Çoğu programcı yüksek seviyeli bir model olmadan kodlamaya başlar ve bu da tasarım hatalarına yol açar
- TLA+, kodun ne yaptığını ve nasıl davrandığını açıkça tanımlayabilen yüksek seviyeli bir model dilidir
- Sistem ne kadar karmaşıksa sadeleştirme o kadar önemlidir; bu, kod yazma becerisiyle değil daha üst düzey düşünmeyle sağlanır
- Bir endüstriyel projede TLA+ modelleme sayesinde gerçek zamanlı işletim sisteminin kod boyutunun onda bire indirildiği bir örnek vardır
- Modelleme, tasarım hatalarını önceden bulmada etkilidir ve test ya da kod düzeltmeye kıyasla daha güvenilirdir
Paralel sistem modelleme
- Paralel sistemler, aynı anda çalışan birden çok bileşenden (süreçten) oluşur
- Dağıtık sistemlerde mekânsal olarak ayrılmış süreçler mesajlar üzerinden iletişim kurar
- TLA+, tüm sistem durumunu küresel durum olarak modeller
- 40 yılı aşkın deneyime göre, dağıtık sistemleri küresel durum temelli olarak modellemek en genel anlamda en kullanışlı yaklaşımdır
Durum makinesi (State Machine)
- TLA+, eylem kümesini şu iki öğeyle tanımlar:
- Başlangıç koşulu: olası başlangıç durumlarını belirtir
- Sonraki durum ilişkisi: olası adımları (ardışık durum çiftlerini) belirtir
- Bu iki koşulu sağlayan eylemler kümesi modeldir
- Bu tür modellere durum makinesi (state machine) denir
- Sonlu durum makinesi (finite-state machine), durum sayısı sonlu olan bir durum makinesidir
- Turing makinesi bir durum makinesi örneğidir; deterministik Turing makinesinde her durum için en fazla bir sonraki durum vardır
- Bir programlama dilinin anlamını tam ve pratik biçimde açıklamanın yolu, onu durum makinesine dönüştüren işlemsel anlambilimdir
- Sonraki durum eylemi yalnızca gerçekleşebilecek adımları belirtir; bunların mutlaka gerçekleşeceği anlamına gelmez
- Bir adımın zorunlu olarak gerçekleşmesini belirtmek için adillik koşulu (fairness property) eklenmelidir
- Adillik olmadan da komisyon türü hataları bulmak yeterince mümkündür, ancak ihmal türü hatalar tespit edilmez
- Çoğu durumda hatalar daha çok commission türündedir; yeni başlayanlar başlangıç koşulu ve sonraki durum ilişkisini yazmakla başlamalıdır
Özellik doğrulama
- Sistemin istenildiği gibi çalışıp çalışmadığını kontrol etmek için model yazılır
- Modelin olası tüm davranışlar için belirli bir özelliği sağlayıp sağlamadığı TLA+ araçlarıyla doğrulanabilir
- Örneğin, başlangıç durumlarının %99'unda çalışma normal biçimde sonlansa bile, tüm davranışların normal biçimde sonlanması gerektiği doğrulanır
- En yaygın özellik, her durumda her zaman doğru olması gereken değişmezlik özelliğidir (invariance property)
- Adillik koşulu içeren modellerde canlılık özelliği (liveness property) de doğrulanmalıdır → örneğin çalışmanın mutlaka sonlanması
- Daha karmaşık özellikler durum makinesiyle ifade edilebilir ve başka bir durum makinesinin bunu gerçekleştirip gerçekleştirmediği doğrulanabilir
- TLA+'ta durum makinesi ile özellik arasında biçimsel bir ayrım yoktur; ikisi de aynı şekilde matematiksel formülle ifade edilir
- Bir durum makinesinin başka bir durum makinesini gerçekleştirmesi, ilgili formülün mantıksal olarak içerilmesi anlamına gelir
- Pratikte çoğunlukla yalnızca değişmezlik ve basit canlılık özellikleri denetlenir, ancak daha karmaşık kavramları anlamak da kod hatalarını önlemeye yardımcı olur
TLA+ dilinin kendisi
- TLA+, matematik temelli bir dildir ve bir programlama dili gibi görünmez
- Programcılar matematiksel ifadelerden çok programlama dillerine alışık oldukları için ilk başta zor gelebilir
- Ancak gerçekte matematik, programlama dillerinden daha yüksek ifade gücüne sahiptir
- Örneğin GCD, iki sayıyı bölen en büyük pozitif tam sayı olarak tanımlanabilir (hesaplama yöntemi belirtilmeden)
- Matematiksel tanımlar, amaç için gerekli özü bırakıp gereksiz uygulama ayrıntılarını soyutlayabilir
- Prosedürel hale getirme soyutlama sağlamaz; yalnızca kodu başka bir yerde gizler
- PlusCal, TLA+ öğrenmeye başlamak için uygundur ve deneyimli kullanıcılar da basit modellerde PlusCal'i tercih eder
- Ancak matematiksel düşünmek ve yüksek seviyeli modelleme yapmak için TLA+'ın kendisini öğrenmek önemlidir
3 yorum
https://cacm.acm.org/research/… AWS'de iyi kullanılıyor.
Kodlama programlama değildir
Bu yazıda bahsedildiği için ben de araştırdım.
Ben de bu yazıda ilk kez gördüm, o yüzden araştırıyordum.