检索结果-内蒙古大学图书馆

Evaluating and designing software mutual exclusion algorithms on shared-memory multiprocessors

IEEE PARALLEL & DISTRIBUTED TECHNOLOGY 1996年第1期4卷 25-42页

作者： Zhang, XD Yan, Y Castaneda, R High-Performance Computing and Software Laboratory University of Texas San Antonio USA

Performance evaluations of software-based mutual exclusion algorithms must take into account the effects of architectures and systems. The authors demonstrate ate a framework for such evaluation, and use the framework... 详细信息

关键词： Cache Coherence Memory Hierarchy mutual exclusion algorithms Performance Evaluation And Shared Memory Multiprocessor Systems

来源：评论

学校读者我要写书评

暂无评论

Verifying mutual exclusion algorithms with Non-Atomic Registers

引用

algorithms 2024年第12期17卷 536-536页

作者： Nigro, Libero Univ Calabria DIMES I-87036 Arcavacata Di Rende Italy

The work described in this paper develops a formal method for modeling and exhaustive verification of mutual exclusion algorithms. The process is based on timed automata and the Uppaal model checker. The technique was successfully applied to several mutual exclusion algorithms, mainly under the atomic memory model, when the read and write operations on memory cells (registers) are atomic or indivisible. The original contribution of this paper consists of a generalization of the approach to support modeling mutual exclusion algorithms with non-atomic registers, where multiple read operations can occur on a register simultaneously to a write operation on the same register, thus giving rise to the flickering phenomenon or multiple write operations can occur at the same time on the same register, hence determining the scrambling phenomenon. The paper first clarifies some consistency rules of non-atomic registers. Then, the developed Uppaal-based method for specifying and verifying mutual exclusion algorithms is presented. The method is applied to the correctness assessment of a sample mutual exclusion solution. After that, non-atomic register consistency rules are rendered in Uppaal to be embedded in the specification methodology. The paper goes on by presenting different mutual exclusion algorithms that are studied using non-atomic registers. algorithms are also investigated in the context of a tournament tree organization that can provide standard and efficient mutual exclusion solutions for N>2 processes. The paper compares the proposed techniques for handling non-atomic registers and reports about their application to many other mutual exclusion solutions.

关键词： mutual exclusion algorithms model checking atomic registers non-atomic registers flickering scrambling timed automata Uppaal

来源：评论

学校读者我要写书评

暂无评论

ON THE EQUITY OF mutual exclusion algorithms IN DISTRIBUTED SYSTEMS

引用

INFORMATION PROCESSING LETTERS 1995年第1期56卷 19-22页

作者： GREENWOOD, GW Department of Electrical and Computer Engineering Western Michigan University Kalamazoo MI 49008 USA

In recent years the problem of mutual exclusion in distributed systems has received much attention. The basic problem is to ensure that one and only one site has access to a critical section at any given time. It is suggested that a priority based approach to site selection in token-based mutual exclusion algorithms is better than selection criteria based solely upon timestamps or counters. Sites needing frequent access to a critical section should not spend an inordinate amount of time blocked for sites needing fewer accesses. The overall schedule length of the distributed computation should improve if the sites needing many accesses to a critical section are more unlikely to be blocked.

关键词： DISTRIBUTED SYSTEMS mutual exclusion algorithms

来源：评论

学校读者我要写书评

暂无评论

Automated analysis of mutual exclusion algorithms using CCS

引用

Formal Aspects of Computing 1989年第1期1卷 273-292页

作者： Walker, D.J. Department of Computer Science University of Edinburgh Edinburgh EH9 3JZ United Kingdom

A number of mutual exclusion algorithms are studied by representing them as agents in the Calculus of Communicating Systems and using an automated tool embodying some of the theory of the Calculus to analyse the representations. It is determined whether or not each of the algorithms preserves mutual exclusion and is live. © 1989 BCS.

关键词： CCS Concurrency workbench mutual exclusion algorithms

来源：评论

学校读者我要写书评

暂无评论

Modelling and Verification of mutual exclusion algorithms 16

Modelling and Verification of Mutual Exclusion Algorithms

引用

20th IEEE/ACM International Symposium on Distributed Simulation and Real Time Applications (DS-RT)

作者： Cicirelli, Franco Nigro, Libero CNR Natl Res Council Italy Inst High Performance Comp & Networking ICAR I-87036 Arcavacata Di Rende CS Italy Univ Calabria Dept Informat Modelling Elect & Syst Sci DIMES Arcavacata Di Rende CS Italy

ISBN: (纸本)9781509035052

This paper proposes modelling and exhaustive verification of mutual exclusion algorithms using timed automata (TA) and the popular UPPAAL toolbox. The proposal allows to check all the properties of a mutual exclusion algorithm also along the time dimension. Both the classic case of atomic read/write operations on memory cells and the non determinism of reading a memory cell during one or multiple write operations on it as it may occur in modern multi-port memories are considered. The approach is then applied to some algorithms proposed in the literature of which known properties are confirmed but also new ones are revealed.

关键词： mutual exclusion algorithms atomic vs. non atomic read/write operations timed automata model checking UPPAAL

来源：评论

学校读者我要写书评

暂无评论

Verification of mutual exclusion algorithms with SMV System 2

Verification of mutual exclusion algorithms with SMV System

引用

International Conference on Computer as a Tool

作者： Bogunovic, N Pek, E Fac Elect & Comp Engn Zagreb Croatia

ISBN: (纸本)078037763X

mutual exclusion algorithms can exhibit intricate behavior for which correctness can be hard to establish. We demonstrate automatic verification of five algorithms by symbolic model checking. We used SMV too I which enables property specification in computation tree logic and allow us to impose fairness constraints on a model. For each of the algorithm we verify safety, liveness, non-blocking and no strict ordering properties.

关键词： formal verification model checking mutual exclusion algorithms CTL SMV

来源：评论

学校读者我要写书评

暂无评论

Formalization of mutual exclusion algorithms in N-labeled Calculus 7

Formalization of Mutual Exclusion Algorithms in <i>N</i>-lab...

引用

IEEE 7th Joint International Information Technology and Artificial Intelligence Conference (ITAIC)

作者： Mizutani, Tetsuya Tomita, Kohji Univ Tsukuba Fac Engn Informat & Syst Tsukuba Ibaraki Japan AIST Intelligent Syst Res Inst Tsukuba Ibaraki Japan

ISBN: (纸本)9781479944194

A family of formal systems called "labeled calculi" have been investigated lately for verification and analysis of time-concerned cooperating program systems. These calculi have high formality since they are based on the Peano arithmetic, one of the natural number theories. They are axiom-and proof-based approaches, i.e. properties of systems are verified by formal proofs. These approaches are more rigid and precise than that of model-checking. Among the labeled calculi, N-labeled calculus is the simplest and suited for usual time-concerned programs such as mutual exclusion. mutual exclusion algorithms are indispensable for contemporary programs having parallel tasks/jobs/processes, and they offer typical examples of verification of such time-concerned cooperating programs. In this article, two mutual exclusion algorithms are formally represented in the calculus for verification.

关键词： mutual exclusion algorithms Formalism N-labeled calculus

来源：评论

学校读者我要写书评

暂无评论

Model Checking mutual exclusion algorithms Using UPPAAL 1

引用

5th Computer Science On-line Conference (CSOC)

作者： Cicirelli, Franco Nigro, Libero Sciammarella, Paolo F. Univ Calabria Dept Informat Modelling Elect & Syst Sci DIMES Arcavacata Di Rende CS Italy

ISBN: (数字)9783319336220

ISBN: (纸本)9783319336220;9783319336206

This paper proposes an approach to modelling and exhaustive verification of mutual exclusion algorithms which is based on Timed Automata in the context of the popular UPPAAL toolbox. The approach makes it possible to study the properties of a mutual exclusion algorithm also in the presence of the time dimension. For demonstration purposes some historical algorithms are modelled and thoroughly analyzed, going beyond some informal reasoning reported in the literature. The paper also proposes a mutual exclusion algorithm for N >= 2 processes whose model checking confirms it satisfies all the required properties.

关键词： mutual exclusion algorithms Model checking Timed automata UPPAAL

来源：评论

学校读者我要写书评

暂无评论

IMPROVED PERFORMANCE EVALUATION OF DISTRIBUTED mutual exclusion algorithms FOR COMPUTER-NETWORKS

引用

COMPUTING SYSTEMS 1993年第2期8卷 67-71页

作者： HOFFMAN, LL UNIV CENT FLORIDA DEPT STATORLANDOFL 32816

Steady state queue depth probabilities are critical for evaluating average waiting times in computer networks. An improvement to the analytical approach of Srimani and Mishra is presented in this paper, and then compared to empirical simulation evidence. The proposed expressions are demonstrated to be superior to Srimani and Mishra's.

关键词： mutual exclusion algorithms STEADY STATE QUEUE DEPTH PROBABILITY WAITING TIMES SIMULATION PERFORMANCE EVALUATION

来源：评论

学校读者我要写书评

暂无评论

Formalization of mutual exclusion algorithms in N-labeled Calculus

Formalization of Mutual Exclusion Algorithms in N-labeled Ca...

引用

2014 IEEE 7th Joint International Information Technology and Artificial Intelligence Conference

作者： Tetsuya Mizutani Kohji Tomita Faculty of Engineering Information and SystemsUniversity of Tsukuba Intelligent Systems Research Institute AIST

A family of formal systems called "labeled calculi"have been investigated lately for verification and analysis of timeconcerned cooperating program systems. These calculi have high formality since they are based on the Peano arithmetic, one of the natural number theories. They are axiom- and proof-based approaches, i.e. properties of systems are verified by formal *** approaches are more rigid and precise than that of modelchecking. Among the labeled calculi, N-labeled calculus is the simplest and suited for usual time-concerned programs such as mutual exclusion. mutual exclusion algorithms are indispensable for contemporary programs having parallel tasks/jobs/processes,and they offer typical examples of verification of such timeconcerned cooperating programs. In this article, two mutual exclusion algorithms are formally represented in the calculus for verification.

关键词： mutual exclusion algorithms Formalism N-labeled calculus

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：