Analyzing synchronization objects using theprocess algebra CSP and its model checker FDR
Proses cebiri CSP ve model denetleyicisi FDRkullanarak senkronizasyon nesnelerinin analizi
- Tez No: 918121
- Danışmanlar: PROF. DR. GAVIN LOWE
- Tez Türü: Yüksek Lisans
- Konular: Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve Kontrol, Matematik, Computer Engineering and Computer Science and Control, Mathematics
- Anahtar Kelimeler: Belirtilmemiş.
- Yıl: 2023
- Dil: İngilizce
- Üniversite: University of Oxford
- Enstitü: Yurtdışı Enstitü
- Ana Bilim Dalı: Matematik ve Bilgisayar Bilimleri Ana Bilim Dalı
- Bilim Dalı: Belirtilmemiş.
- Sayfa Sayısı: 108
Özet
Senkronizasyon nesneleri, concurrent (eşzamanlı) programlarda kullanılan senkronizasyon aracılarıdır: Başka iş parçacıkları belirli bir senkronizasyon noktasına ulaşana kadar iş parçacıklarını bloke ederler ve ancak o zaman devam etmelerine izin verirler. Örneğin bir senkron kanal, bir gönderici ve bir alıcı arasında veri iletmek için kullanılır ve her ikisi de diğeri hazır oluncaya kadar bloke olur. Bir başka yaygın örnek olan bariyer, bir concurrent (eşzamanlı) programdaki tüm iş parçacıkları arasında global senkronizasyon sağlamak için kullanılır, yani tüm iş parçacıkları hazır olmadan önce hiçbir iş parçacığı işleme devam edemez. Senkronizasyon doğrusallaştırılabilirliği, senkronizasyonların katılımcı iş parçacıklarının ilgili işlemlerinin çağrılması ve geri dönüşü arasında atomik olarak gerçekleşmesi gerektiğini belirten bir güvenlik özelliğidir. Senkronizasyon ilerleyebilirliği, bir senkronizasyona katılabilecek bekleyen çağrılar olduğunda, sonunda bir senkronizasyonun gerçekleşeceğini ve katılımcı çağrıların sonunda geri döneceğini belirten bir ilerleme özelliğidir. Bu raporda, çeşitli senkronizasyon nesnelerinin önerilen gerçeklemelerinin senkronizasyon doğrusallaştırılabilirliğinin ve senkronizasyon ilerleyebilirliğinin biçimsel doğrulamasını (formal verification) yapıyoruz. İlk olarak proses cebiri CSP'yi kullanarak gerçeklemeyi modelliyor ve ardından istenen davranışı yakalayan onaylama süreçlerini (assertions) kontrol etmek için model denetleyicisi FDR'yi kullanıyoruz. Yaklaşımımızın güçlü ve zayıf yönlerini açıkça ortaya koyuyoruz. Ayrıca analizimizi geliştirmenin probleme özgü yollarını da gösteriyoruz.
Özet (Çeviri)
Synchronization objects are mediators of synchronization in concurrent programs: They block threads until some other threads reach a certain synchronization point and only then, they allow them to continue. A synchronous channel, for example, is used to transmit data between a sender and a receiver where both of them block until the other becomes available. A barrier, another common example, is used to achieve global synchronization between all threads in a concurrent program, i.e. no thread can proceed before all threads are available. Synchronization linearizability is a safety property that states synchronizations must appear to take place atomically between the invocation and return of participating threads' respective operations. Synchronization progressability is a progress property that states whenever there are pending invocations that can participate in a synchronization, a synchronization eventually takes place and participating invocations eventually return. In this report, we formally verify synchronization linearizability and synchronization progressability of proposed implementations of various synchronization objects. We first model the implementation using the process algebra CSP and then use its model checker FDR to check assertions capturing desired behaviour. We make strengths and weaknesses of our approach clear. We also demonstrate problem-specific ways of improving our analysis.
Benzer Tezler
- DNS big data processing for detecting customersbehaviour of isp using an optimized apache spark cluster
İSP müşterilerin davranışlarını tespiti için optimize edilmiş bir apache spark kümesi kullanarak dns büyük veri işleme
YOUSEF ALKHANAFSEH
Yüksek Lisans
İngilizce
2022
Elektrik ve Elektronik Mühendisliğiİstanbul Teknik ÜniversitesiElektrik ve Elektronik Mühendisliği Ana Bilim Dalı
PROF. DR. TAHİR ÇETİN AKINCI
- Federe öğrenme kullanılarak nesnelerin interneti (IOT) verileri analizi
Analyzing internet of things (IOT) data using federated learning
SÜLEYMAN BURAK ALTINIŞIK
Yüksek Lisans
Türkçe
2025
Bilgisayar Mühendisliği Bilimleri-Bilgisayar ve KontrolBursa Teknik ÜniversitesiBilgisayar Mühendisliği Ana Bilim Dalı
PROF. DR. TURGAY TUGAY BİLGİN
- RF tabanlı hedef konumlandırma sistemleri
RF based target positioning systems
MAHMUT GÜLNAZ
Yüksek Lisans
Türkçe
2016
Elektrik ve Elektronik MühendisliğiHacettepe ÜniversitesiElektrik-Elektronik Mühendisliği Ana Bilim Dalı
YRD. DOÇ. YAKUP SABRİ ÖZKAZANÇ
- Empirical analyses on convergence triggers in Africa, structural symmetry and transmission mechanisms in transition to the East African Monetary Union
Afrika'da yakınsamanın tetikleyicileri üzerine ampirik analiz, Doğu Afrika Parasal Birliğine geçişte yapısal simetri ve aktarım mekanizmaları
AWENG PETER MAJOK GARANG
- Güverte tayfasının çalışma periyoduna bağlı olarak gelişen psikofizyolojik verilerinin liman operasyonu süreçlerinde analizi
Analyzing the deck ratings' psychophysiological datas due to working period during port operations
BARIŞ ÖZSEVER
Yüksek Lisans
Türkçe
2015
Denizcilikİstanbul Teknik ÜniversitesiDeniz Ulaştırma Mühendisliği Ana Bilim Dalı
DOÇ. DR. LEYLA TAVACIOĞLU