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

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 1993年第1期15卷 73-132页

作者： ABADI, M LAMPORT, L Digital Equipment Corp. Palo Alto CA Digital Equipment Corp. Palo Alto CA

A rigorous modular specification method requires a proof rule asserting that if each component behaves correctly in isolation, then it behave correctly in concert with other components. Such a rule is subtle because a component need behave correctly only when its environment does, and each component is part of the others' environments. We examine the precise distinction between a system and its environment, and provide the requisite proof rule when module 8 are specified with safety and liveness properties.

关键词： COMPOSITIONALITY concurrent programming LIVENESS PROPERTIES MODULAR SPECIFICATION SAFETY PROPERTIES

来源：评论

学校读者我要写书评

暂无评论

A deadlock detection tool for concurrent Java programs

引用

SOFTWARE-PRACTICE & EXPERIENCE 1999年第7期29卷 577-603页

作者： Demartini, C Iosif, R Sisto, R Politecn Torino Dipartimento Automat & Informat I-10129 Turin Italy

This paper presents some issues related to the design and implementation of a concurrency analysis toot able to detect deadlock situations in Java programs that make use of multithreading mechanisms. An abstract formal model is generated from the Java source using the Java2Spin translator. The model is expressed in the PROMELA language, and the SPIN tool is used to perform its formal analysis, The paper mainly focuses on the design of the Java2Spin translator. A set of experiments, carried out to evaluate the performances of the analysis tool, is also presented. Copyright (C) 1999 John Whey & Sons, Ltd.

关键词： concurrent programming deadlock formal analysis Java PROMELA SPIN

来源：评论

学校读者我要写书评

暂无评论

Backend pro kolaborativní programování v rozšířené realitě

Backend pro kolaborativní programování v rozšířené re...

引用

作者： Willaschek, Tomáš Brno University of Technology

Tato práce se zabývá implementací a aplikací výlučného přístupu pro systém ARCOR2, který slouží ke kolaborativnímu programování robotů v rozší... 详细信息

Tato práce se zabývá implementací a aplikací výlučného přístupu pro systém ARCOR2, který slouží ke kolaborativnímu programování robotů v rozšířené realitě. Cílem práce je analýza výchozího stavu, návrh a implementace výlučného přístupu pro tento systém. Implementace je rozsáhlá a umožňuje řadu pracovních scénářů, které vyžadují aplikaci výlučného přístupu. Tyto scénáře jsou odhaleny analýzou systému. Na tomto základu je vytvořen návrh, který řeší problematické scénáře. Nedostatek systému je vyřešen vytvořením globálního manažera zámků, který je aplikován. V rámci práce jsou definovány vzory, jak manažera zámků použít. Přínosem práce je efektivní a nekonfliktní kolaborativní programování.

关键词： výlučný přístup zamykání v AsyncIO konkurentní programování rozšířená realita exclusive access AsyncIO lock concurrent programming augmented reality Text

来源：评论

学校读者我要写书评

暂无评论

PhTM*: uma implementação eficiente de transações em fases

PhTM*: uma implementação eficiente de transações em fase...

引用

作者： Carvalho, João Paulo Labegalini de Universidade Estadual Paulista

As evidentes limitações em se explorar o aumento de frequência e otimização no nível de microarquitetura para obtenção de desempenho levaram a indústria de microprocessador... 详细信息

As evidentes limitações em se explorar o aumento de frequência e otimização no nível de microarquitetura para obtenção de desempenho levaram a indústria de microprocessadores a buscar alternativas para suprir tal demanda. A solução encontrada foi construir arquiteturas com múltiplos fluxos de execução (multicore). No entanto, a utilização imediata do modelo paralelo exige que os programadores precisem explicitamente codificar as aplicações de forma a usar todos os núcleos, tarefa essa nada trivial e passível de erros que, muitas vezes, são difíceis de serem detectados. Um novo modelo de programação concorrente conhecido como memória transacional (Transactional Memory – TM) oferece abstrações para fácil codificação de aplicações e é capaz de explorar o paralelismo das arquiteturas multicore sem exigir conhecimentos da arquitetura por parte do programador. Porém, as implementações desse modelo, em software ou hardware, isoladamente apresentam problemas que limitam a escalabilidade das aplicações. Objetivando resolver tais problemas, foram propostos sistemas híbridos de transações em hardware e software para melhor exploração do paralelismo, denominado Memória Transacional Híbrida (Hybrid Transactional Memory – HyTM). A flexibilidade dos sitemas híbridos convencionais, mesmo permitindo executar transações em hardware e software simultaneamente, reduzem o desempenho de ambos seus componentes e tornam mais complexa a implementação da componente em software. Nesse sentido, este trabalho apresenta a primeira implementação eficiente (PhTM*) de um sistema de transações em fases, proposto como alternativa aos HyTMs convencionais. O PhTM* elimina a instrumentação das transações em hardware, necessária em outros HyTMs, e permite utilizar qualquer STM, sem nenhuma modificação, para executar as transações em software. A proposta é a primeira a utilizar o suporte transacioal em hardware disponível em um processador real (não-emulado), para executar as transações em hardware. Os re

关键词： Programação concorrente Memória transacional Sistemas híbridos Fases do programa concurrent programming Transactional memory Hybrid systems Program phase Dissertação de mestrado

来源：评论

学校读者我要写书评

暂无评论

PARFORMAN - An assertion language for specifying behavior when debugging parallel applications

引用

INTERNATIONAL JOURNAL OF SOFTWARE ENGINEERING AND KNOWLEDGE ENGINEERING 1996年第4期6卷 609-640页

作者： Auguston, M Fritzson, P NEW MEXICO STATE UNIV DEPT COMP SCI LAS CRUCES NM 88003 USA LINKOPING UNIV DEPT COMP & INFORMAT SCI S-58183 LINKOPING SWEDEN

PARFORMAN (PARallel FORMal ANnotation language) is a high-level specification language for expressing intended behavior or known types of error conditions when debugging or testing parallel programs. Models of intended or faulty target program behavior can be succinctly specified in PARFORMAN. These models are then compared with the actual behavior in terms of execution traces of events, in order to localize possible bugs. PARFORMAN can also be used as a general language for expressing computations over target program execution histories. PARFORMAN is based on a precise model of target program behavior. This model, called H-space (History-space), is formally defined through a set of general axioms about three basic relations, which may or may not hold between two arbitrary events: they may be sequentially ordered (SEQ), they may be parallel (PAR), or one of them might be included in another composite event (IN). The general notion of composite event is exploited systematically, which makes possible more powerful and succinct specifications. The notion of event grammar is introduced to describe allowed event patterns over a certain application domain or language. Auxiliary composite events such as Snapshots are introduced to be able to define the notion ''occurred at the same time'' at suitable levels of abstraction. Finally, patterns and aggregate operations on events are introduced to make possible short and readable specifications. In addition to debugging and testing, PARFORMAN can also be used to specify profiles and performance measurements.

关键词： annotation language assertions testing debugging concurrent programming occam parallelism

来源：评论

学校读者我要写书评

暂无评论

THE TEMPORAL LOGIC OF ACTIONS

引用

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 1994年第3期16卷 872-923页

作者： LAMPORT, L Digital Equipment Corp. Palo Alto CA

The temporal logic of actions (TLA) is a logic for specifying and reasoning about concurrent systems. Systems and their properties are represented in the same logic, so the assertion that a system meets its specification and the assertion that one system implements another are both expressed by logical implication. TLA is very simple;its syntax and complete formal semantics are summarized in about a page. Yet, TLA is not just a logician's toy;it is extremely powerful, both in principle and in practice. This report introduces TLA and describes how it is used to specify and verify concurrent algorithms. The use of TLA to specify and reason about open systems will be described elsewhere.

关键词： THEORY VERIFICATION concurrent programming LIVENESS PROPERTIES SAFETY PROPERTIES

来源：评论

学校读者我要写书评

暂无评论

Practical proofs of concurrent programs

引用

ACM SIGPLAN NOTICES 2006年第9期41卷 123-123页

作者： Shapiro, Marc INRIA Rocquencourt & LIP6 Project Regal F-75015 Paris France

Modern computer architectures are increasingly parallel: viz., clusters and multi-core PCs. More and more developers will be seduced into concurrent programming, unprepared for the difficulties of understanding, writing and debugging concurrent programs. Proposed higher-level abstractions (such as lightweight transactions [3]) may provide the illusion that concurrency is easy, but there is a fundamental theoretical issue: threads can interfere with one another in arbitrary ways;the number of cases is combinatorial. In practice however, reasonable programs have concurrency control disciplines (e.g., locking) that avoid the bad interactions. We propose to formalise this concurrency control and to leverage it, in order to reason in a modular fashion and side-step the combinatorial explosion. To this effect, we use the "rely-guarantee" (R-G) approach [1, 4]. In addition to the standard pre- and post-conditions of sequential Hoare logic, a program is equipped with a non-interference assertions: a rely condition limits the interference it may suffer from its environment;a guarantee condition specifies what interference it may inflict on its environment. If the rely condition of any particular thread is implied by all other threads' guarantee conditions (and if certain technical conditions are met), then standard sequential reasoning can be used to prove the post-condition. We describe some extensions to the basic R-G approach to make it practical. As an example, we study a family of implementations for linked lists using fine-grain synchronisation. This approach enables greater concurrency, but correctness is a greater challenge than for classical, coarse-grain synchronisation. Our examples are demonstrative of common design patterns such as lock coupling, optimistic, and lazy synchronisation. Although they are highly con-current, we prove that they are linearisable, safe, and they correctly implement a high-level abstraction [5]. With this work, we learned that the exten

关键词： assertions concurrent programming program proofs Hoare logic rely-guarantee

来源：评论

学校读者我要写书评

暂无评论

Přesné heuristiky pro vkládání šumu v nástroji SearchBestie

Přesné heuristiky pro vkládání šumu v nástroji Search...

引用

作者： Kozák, David Brno University of Technology

Tato práce se zabývá efektivními způsoby testování vícevláknových programů psaných v jazyce Java. Pro zvýšení šance na odhalení časově závislý... 详细信息

Tato práce se zabývá efektivními způsoby testování vícevláknových programů psaných v jazyce Java. Pro zvýšení šance na odhalení časově závislých chyb se využívá techniky vkládání šumu, kdy dochází ke vložení dalších instrukcí do testované aplikace za účelem prozkoumání netypických proložení událostí. Pro nalezení vhodných konfigurací pro vkládání šumu byl navržen nástroj SearchBestie, který využíval nástroj ConTest pro spouštění testů a instrumentaci bytecodu. Jelikož vývoj ConTestu byl zastaven, bylo třeba najít vhodnou alternativu. V průběhu této bakalářské práce bylo dokončeno propojení SearchBestie s nástrojem RoadRunner, který ConTest nahradil. Dále došlo k navržení a implementaci nových heuristik, které umožňují šum vkládat na přesně zvolená místa v kódu. Experimenty prokázaly, že ve většině případů skutečně přesné heuristiky dosahují lepších výsledků než heuristiky využívající náhodnosti.

关键词： verifikace softwaru testování vícevláknové programování Java chyby ve vícevláknových programech vkládání šumu metriky pro testování software verification testing concurrent programming Java concurrency errors noise injection metrics for testi

来源：评论

学校读者我要写书评

暂无评论

Correctness of an STM Haskell Implementation

引用

ACM SIGPLAN NOTICES 2013年第9期48卷 161-172页

作者： Schmidt-Schauss, Manfred Sabel, David Goethe Univ Frankfurt Frankfurt Germany

A concurrent implementation of software transactional memory in concurrent Haskell using a call-by-need functional language with processes and futures is given. The description of the small-step operational semantics is precise and explicit, and employs an early abort of conflicting transactions. A proof of correctness of the implementation is given for a contextual semantics with may- and should-convergence. This implies that our implementation is a correct evaluator for an abstract specification equipped with a bigstep semantics.

关键词： Languages Theory Verification Functional programming concurrent programming Semantics Software Transactional Memory Haskell

来源：评论

学校读者我要写书评

暂无评论

WIN AND SIN - PREDICATE TRANSFORMERS FOR CONCURRENCY

引用

ACM TRANSACTIONS ON programming LANGUAGES AND SYSTEMS 1990年第3期12卷 396-428页

作者： LAMPORT, L Digital Equipment Corp. Palo Alto CA

The weakest liberal precondition and strongest postcondition predicate transformers are general- ized to the weakest invariant and strongest invariant. These new predicate transformers are useful for reasoning about concurrent programs containing operations in which the grain of atomicity is unspecied. They can also be used to replace behavioral arguments with more rigorous assertional ones.

关键词： concurrent programming Invariance Safety properties Predicate transformers

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：