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

21st Ada-Europe International conference on Reliable Software Technologies (Ada-Europe)

作者： Mazzanti, Franco CNR ISTI Ist Sci & Tecnol Informaz A Faedo Pisa Italy

ISBN: (纸本)9783319390833;9783319390826

Even if multicore architectures are nowadays extremely wide- spread, the exploitation of this easily available degree of parallelism is not always straightforward. In this paper we describe the experience gained in our ongoing effort to parallelise the model checking engine of a family of model checkers (KandISTI) developed at ISTI. The main focus of our experimentation is the evaluation of the minimal efforts needed to take advantage of our everyday multicore hardware for model checking purposes. Our early results relative to an initial fragment of the logic show a speedup factor of about 2.5 when 4 physical cores are available. This result, however, can only be achieved by complementing the initial high level Ada design with a second round of code fine- tuning which exploits nonstandard low level features in the implementation of the needed thread-safe data structures.

关键词： Model checking Parallel programming Multicore processor architectures Ada programming language

来源：评论

学校读者我要写书评

暂无评论

From network interface to multithreaded web applications : A case study in modular program verification 15

From network interface to multithreaded web applications : A...

引用

42nd Annual acm sigplan-SIGACT Symposium on Principles of programming languages, POPL 2015

作者： Chlipala, Adam MIT CSAIL United States

ISBN: (纸本)9781450333009

Many verifications of realistic software systems are monolithic, in the sense that they define single global invariants over complete system state. More modular proof techniques promise to support reuse of component proofs and even reduce the effort required to verify one concrete system, just as modularity simplifies standard software development. This paper reports on one case study applying modular proof techniques in the Coq proof assistant. To our knowledge, it is the first modular verification certifying a system that combines infrastructure with an application of interest to end users. We assume a nonblocking API for managing TCP networking streams, and on top of that we work our way up to certifying multithreaded, database-backed Web applications. Key verified components include a cooperative threading library and an implementation of a domain-specific language for XML processing. We have deployed our case-study system on mobile robots, where it interfaces with off-the-shelf components for sensing, actuation, and control. Copyright © 2015 by the Association for Computing Machinery, Inc. (acm).

关键词： Software design

来源：评论

学校读者我要写书评

暂无评论

Proceedings of the 1986 acm conference on LISP and Functional programming, LFP 1986

Proceedings of the 1986 ACM Conference on LISP and Functiona...

引用

1986 acm conference on LISP and Functional programming, LFP 1986

ISBN: (纸本)0897912004

The proceedings contain 32 papers. The topics discussed include: a simple applicative language: Mini-ML;the CURRY Chip;desiderata for the standardisation of LISP;laws in Miranda;variations on strictness analysis;experience with an uncommon Lisp;an architecture for mostly functional languages;integrating functional and imperative programming;code generation techniques for functional languages;the implementation of PC scheme;design of an optimising, dynamically retargetable compiler for common Lisp;expansion-passing style: beyond conventional macros;the four-stroke reduction engine;LISP on a reduced-instruction-set-processor;hygienic macro expansion;partitioning parallel programs for macro-dataflow;exact real arithmetic: a case study in higher order programming;NORMA: a graph reduction processor;reconfigurable, retargetable bignums: a case study in efficient, portable Lisp system building;implementing functional languages in the categorical abstract machine;connection graphs;connection machine@ Lisp: pine-grained parallel symbolic processing;and the mystery of the tower revealed: a non-reflective description of the reflective tower.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Compressing Java class files

Proceedings of the ACM SIGPLAN Conference on Programming Lan...

引用

Proceedings of the acm sigplan conference on programming language design and implementation (PLDI) 1999年 247-258页

作者： Pugh, William Univ of Maryland College Park MD United States

Java class files are often distributed as jar files, which are collections of individually compressed class files (and possibility other files). Jar files are typically about 1/2 the size of the original class files due to compression. I have developed a wire-code format for collections of Java class files. This format is typically 1/2 to 1/5 of the size of the corresponding compressed jar file (1/4 to 1/10 the size of the original class files).

关键词： Java programming language

来源：评论

学校读者我要写书评

暂无评论

A practical type system and language for reference immutability 04

A practical type system and language for reference immutabil...

引用

19th Annual acm conference on Object-Oriented programming, Systems, languages, and Applications, OOPSLA'04

作者： Birka, Adrian Ernst, Michael D. MIT Comp. Sci./Artif. Intell. Lab. Cambridge MA 02139 United States

ISBN: (纸本)1581138318

This paper describes a type system that is capable of expressing and enforcing immutability constraints. The specific constraint expressed is that the abstract state of the object to which an immutable reference refers cannot be modified using that reference. The abstract state is (part of) the transitively reachable state: that is, the state of the object and all state reachable from it by following references. The type system permits explicitly excluding fields or objects from the abstract state of an object. For a statically type-safe language, the type system guarantees reference immutability. If the language is extended with immutability downcasts, then run-time checks enforce the reference immutability constraints. In order to better understand the usability and efficacy of the type system, we have implemented an extension to Java, called Javari, that includes all the features of our type system. Javari is interoperable with Java and existing JVMs. It can be viewed as a proposal for the semantics of the Java const keyword, though Javari's syntax uses readonly instead. This paper describes the design and implementation of Javari, including the type-checking rules for the language. This paper also discusses experience with 160,000 lines of Javari code. Javari was easy to use and provided a number of benefits, including detecting errors in well-tested code.

关键词： Object oriented programming

来源：评论

学校读者我要写书评

暂无评论

Proceedings of the acm SIGAda Annual International conference;SIGAda

Proceedings of the ACM SIGAda Annual International Conferenc...

引用

1998 Annual acm SIGAda International conference on Ada, SIGAda 1998

ISBN: (纸本)1581130333

The proceedings contain 37 papers. The topics discussed include: multi-μ: an Ada 95 based architecture for fault tolerance support of real-time systems;a comparison of Ada and Pascal in an introductory computer science course;a reusable lightweight executive for command and control systems;hardware/software co-design: VHDL and Ada 95 code migration and integrated analysis;kernel Ada to unify hardware and software design;a empirical study of web-based algorithm animation courseware in an Ada data structure course;using Ada in non-CS majors;the Ravenscar tasking profile for high integrity real-time programs;the evolution of a distributed dataflow processing model using Ada;building fault tolerant distributed systems using IP multicast;looking into safety with the safety and security Rapporteur group;an ASIS-based static analysis tool for high-integrity systems;Ada in embedded boards for scientific and medical instruments;implementing a culling and self-intersection algorithm for stereolithography files in Ada 95;reusable Ada libraries supporting infinite data structures;Ada in an on-board military communication system;a large distributed control system using Ada in Fusion Research;reengineering a legacy system using design patterns and Ada-95 object-oriented features;usage of Ada in the Gripen flight control system;and visual support for incremental abstraction and refinement in Ada 95.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Checking race freedom via linear programming

引用

acm sigplan NOTICES 2008年第6期43卷 1-10页

作者： Terauchi, Tachio Tohoku Univ Sendai Miyagi 980 Japan

We present a new static analysis for race freedom and race detection. The analysis checks race freedom by reducing the problem to ( rational) linear programming. Unlike conventional static analyses for race freedom or race detection, our analysis avoids explicit computation of locksets and lock linearity/must-aliasness. Our analysis can handle a variety of synchronization idioms that more conventional approaches often have difficulties with, such as thread joining, semaphores, and signals. We achieve efficiency by utilizing modern linear programming solvers that can quickly solve large linear programming instances. This paper reports on the formal properties of the analysis and the experience with applying an implementation to real world C programs.

关键词： algorithms languages theory verification fractional capabilities linear programming

来源：评论

学校读者我要写书评

暂无评论

Analysis, design and implementation of an object-oriented framework in Ada95 5th

引用

5th Ada-Europe International conference on Reliable Software Technologies

作者： Schmitt, D Sema Grp GmbH D-26389 Wilhelmshaven Germany Open Univ Milton Keynes MK7 6AA Bucks England

ISBN: (纸本)3540676694

This paper describes the analysis, design and implementation of an object-oriented framework for discrete event simulation in the programming language Ada95. The framework was constructed in an industrial setting so that conclusions are drawn from first-hand, practical experience with this approach. After defining the term 'Object-Oriented Framework', discrete event simulation is analyzed as the domain of concern in the given context, producing a class diagram for that domain in the Unified Modelling language (UML). Following the analysis activities, the framework is designed and described, again using diagrams of the UML. In further sections the mapping from design artifacts to code in Ada95 and the usage of the framework are shown. The article finishes with a summary of the experience gained and the lessons learned.

关键词： frameworks object-oriented technologies experience reports from projects using Ada95 case studies and experiments

来源：评论

学校读者我要写书评

暂无评论

Multi-dispatch in the Java Virtual Machine: design and implementation

Multi-dispatch in the Java Virtual Machine: Design and imple...

引用

2000 conference on Object-Oriented programming, Systems, languages, and Applications, OOPSLA 2000

作者： Dutchyn, Christopher Lu, Paul Szafron, Duane Bromling, Steve Holst, Wade Department of Computing Science University of Alberta Edmonton AB T6G 2E8 Canada Department of Computer Science University of Western Ontario MiddleSex College London ON N6A 5B7 Canada

ISBN: (纸本)1581133073

Mainstream object-oriented languages, such as C++ and Java, provide only a restricted form of polymorphic methods, namely single-receiver dispatch. In common programming situations, programmers must work-around this limitation. We detail how to extend the Java Virtual Machine to support multiple-dispatch and examine the complications that Java imposes on multiple-dispatch in practice. Our technique avoids changes to the Java programming language itself, maintains source-code and library compatibility, and isolates the performance penalty and semantic changes of multiple-dispatch to the program sections which use it. We have micro-benchmark and application-level performance results for a dynamic Most Specific Applicable (MSA) dispatcher, two table-based dispatchers (Multiple Row Displacement (MRD) and Single Receiver Projections (SRP)), and a tuned SRP dispatcher. Our general-purpose technique provides smaller dispatch latency than equivalent programmer-written double-dispatch code. © 2000 acm.

关键词： Java programming language

来源：评论

学校读者我要写书评

暂无评论

Aspectual Caml: an aspect-oriented functional language

引用

acm sigplan NOTICES 2005年第9期40卷 320-330页

作者： Masuhara, H Tatsuzawa, H Yonezawa, A Univ Tokyo Grad Sch Arts & Sci Tokyo Japan Univ Tokyo Dept Comp Sci Tokyo Japan Univ Tokyo Dept Comp Sci Tokyo Japan

We propose an aspect-oriented programming (AOP) language called Aspectual Caml based on a strongly-typed functional language Objective Caml with two AOP mechanisms similar to those in AspectJ language. This paper describes the design and implementation issues of those AOP mechanisms that give us insights into the interaction between AOP features and common features in strongly-typed functional languages such as type inference, polymorphic types and curried functions. We implemented a prototype compiler of the language and used the language for separating crosscutting concerns in application programs, including for separating descriptions of a type system from compiler descriptions.

关键词： aspect-oriented programming objective Caml pointcut and advice

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：