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

47th acm/ieee annual International symposium on computer Architecture, ISCA 2020

作者： Zhao, Shulin Zhang, Haibo Bhuyan, Sandeepa Mishra, Cyan Subhra Ying, Ziyu Kandemir, Mahmut T. Sivasubramaniam, Anand Das, Chita R. Pennsylvania State University Dept. of Computer Science and Engineering United States

ISBN: (纸本)9781728146614

the emergence of virtual reality (VR) and augmented reality (AR) has revolutionized our lives by enabling a 360 artificial sensory stimulation across diverse domains, including, but not limited to, sports, media, healthcare, and gaming. Unlike the conventional planar video processing, where memory access is the main bottleneck, in 360 VR videos the compute is the primary bottleneck and contributes to more than 50% energy consumption in battery-operated VR headsets. thus, improving the computational efficiency of the video processing pipeline in a VR is critical. While prior efforts have attempted to address this problem through acceleration using a GPU or FPGA, none of them has analyzed the 360 VR pipeline to examine if there is any scope to optimize the computation with known techniques such as memoization. thus, in this paper, we analyze the VR computation pipeline and observe that there is significant scope to skip computations by leveraging the temporal and spatial locality in head orientation and eye correlations, respectively, resulting in computation reduction and energy efficiency. the proposed Déjà View design takes advantage of temporal reuse by memoizing head orientation and spatial reuse by establishing a relationship between left and right eye projection, and can be implemented either on a GPU or an FPGA. We propose both software modifications for existing compute pipeline and microarchitectural additions for further enhancement. We evaluate our design by implementing the software enhancements on an NVIDIA Jetson TX2 GPU board and our microarchitectural additions on a Xilinx Zynq-7000 FPGA model using five video workloads. Experimental results show that Déjà View can provide 34% computation reduction and 17% energy saving, compared to the state-of-the-art design. © 2020 ieee.

关键词： Edge computing

来源：评论

学校读者我要写书评

暂无评论

UPPER BOUNDS ON thE QUANTIFIER DEPth FOR GRAPH DIFFERENTIATION IN FIRST-ORDER logic

引用

logicAL MEthODS IN computer science 2019年第2期15卷 19:1-19:19页

作者： Kiefer, Sandra Schweitzer, Pascal Rhein Westfal TH Aachen Lehrstuhl Informat 7 Ahornstr 55 D-52074 Aachen Germany TU Kaiserslautern Algorithms & Complex Grp Postfach 3049 D-67663 Kaiserslautern Germany

We show that on graphs with n vertices, the 2-dimensional Weisfeiler-Leman algorithm requires at most O(n(2)/log(n)) iterations to reach stabilization. this in particular shows that the previously best, trivial upper bound of O(n(2)) is asymptotically not tight. In the logic setting, this translates to the statement that if two graphs of size n can be distinguished by a formula in first-order logic with counting with 3 variables (i.e., in C-3), then they can also be distinguished by a C-3-formula that has quantifier depth at most O(n(2)/log(n)). To prove the result we define a game between two players that enables us to decouple the causal dependencies between the processes happening simultaneously over several iterations of the algorithm. this allows us to treat large color classes and small color classes separately. As part of our proof we show that for graphs with bounded color class size, the number of iterations until stabilization is at most linear in the number of vertices. this also yields a corresponding statement in first-order logic with counting. Similar results can be obtained for the respective logic without counting quantifiers, i.e., for the logic L-3.

关键词： first-order logic counting quantifiers Weisfeiler-Leman color refinement

来源：评论

学校读者我要写书评

暂无评论

proceedings of the Joint Meeting of the 23rd EACSL annual Conference on computer science logic, CSL 2014 and the 29th annual acm/ieee symposium on logic in computer science, LICS 2014

Proceedings of the Joint Meeting of the 23rd EACSL Annual Co...

引用

Joint Meeting of the 23rd annual EACSL Conference on computer science logic, CSL 2014 and the 29th annual acm/ ieee symposium on logic in computer science, LICS 2014

ISBN: (纸本)9781450328869

the proceedings contain 76 papers. the topics discussed include: abstract interpretation: past, present and future;computer-checked mathematics: a formal proof of the odd order theorem;citations for the test-of-time award from 1994;infinite-state energy games;beta reduction is invariant, indeed;regular combinators for string transformations*;weight monitoring with linear temporal logic: complexity and decidability*;graph logics with rational relations: the role of word combinatorics;effective interpolation and preservation in guarded logics*;on the discriminating power of passivation and higher-order interaction;a domain-theoretic approach to Brownian motion and general continuous stochastic processes;and two-way cost automata and cost logics over infinite trees*.

关键词：

来源：评论

学校读者我要写书评

暂无评论

On the Satisfiability of Some Simple Probabilistic logics 16

On the Satisfiability of Some Simple Probabilistic Logics

引用

31st annual acm-ieee symposium on logic in computer science (LICS)

作者： Chakraborty, Souymodip Katoen, Joost-Pieter Rhein Westfal TH Aachen Aachen Germany

ISBN: (纸本)9781450343916

this paper shows that the satisfiability problems for a bounded fragment of probabilistic CTL (called bounded PCTL) and an extension of the modal mu-calculus with probabilistic quantification over next-modalities (called P mu TL)are decidable. For bounded PCTL we provide an NEXP-TIME-algorithm for the satisfiability problem and show that the logic has a small model property where the model size is independent from the probability bounds in the formula. We show that the satisfiability problem of a simple sub-logic of bounded PCTL is *** prove that P mu TL has a small model property and that a decision procedure using 2 player parity games can be employed for the satisfiability problem of P mu TL. these results imply that P mu TL and qualitative PCTL formulas with only thresholds >0 and =1-are incomparable. We also establish that-in contrast to PCTL-every satisfiable P mu TL-formula has a rational model, a model with rational probabilities only.

关键词： Probabilistic logic Markov processes Calculus Games Semantics Syntactics Complexity theory

来源：评论

学校读者我要写书评

暂无评论

Order Invariance on Decomposable Structures 16

Order Invariance on Decomposable Structures

引用

31st annual acm-ieee symposium on logic in computer science (LICS)

作者： Elberfeld, Michael Frickenschmidt, Marlin Grohe, Martin Rhein Westfal TH Aachen Aachen Germany

ISBN: (纸本)9781450343916

Order-invariant formulas access an ordering on a structure's universe, but the model relation is independent of the used ordering. they are frequently used for logic-based approaches in computer science. Order-invariant formulas capture unordered problems of complexity classes and they model the independence of the answer to a database query from low-level aspects of databases. We study the expressive power of order-invariant monadic secondorder (MSO) and first-order (FO) logic on restricted classes of structures that admit certain forms of tree decompositions (not necessarily of bounded width). While order-invariant MSO is more expressive than MSO and, even, CMSO (MSO with modulo-counting predicates) in general, we show that order-invariant MSO and CMSO are equally expressive on graphs of bounded tree width and on planar graphs. this extends an earlier result for trees due to Courcelle. Moreover, we show that all properties definable in order-invariant FO are also definable in MSO on these classes. these results are applications of a theorem that shows how to lift up definability results for order-invariant logics from the bags of a graph's tree decomposition to the graph itself.

关键词： finite model theory first-order logic monadic second order logic order-invariant logic modulo-counting logic bounded tree width planarity

来源：评论

学校读者我要写书评

暂无评论

Upper Bounds on the Quantifier Depth for Graph Differentiation in First Order logic 16

Upper Bounds on the Quantifier Depth for Graph Differentiati...

引用

31st annual acm-ieee symposium on logic in computer science (LICS)

作者： Kiefer, Sandra Schweitzer, Pascal Rhein Westfal TH Aachen Aachen Germany

ISBN: (纸本)9781450343916

We show that on graphs with n vertices the 2-dimensional Weisfeiler-Leman algorithm requires at most O(n(2)/log(n)) iterations to reach stabilization. this in particular shows that the previously best, trivial upper bound of O(n(2)) is asymptotically not tight. In the logic setting this translates to the statement that if two graphs of size n can be distinguished by a formula in first order logic with counting with 3 variables (i.e., in C-3) then they can also be distinguished by a C-3-formula that has quantifier depth at most O(n(2)/log(n)). To prove the result we define a game between two players that enables us to decouple the causal dependencies between the processes happening simultaneously over several iterations of the algorithm. this allows us to treat large color classes and small color classes separately. As part of our proof we show that for graphs with bounded color class size, the number of iterations until stabilization is at most linear in the number of vertices. this also yields a corresponding statement in first order logic with counting. Similar results can be obtained for the respective logic without counting quantifiers, i.e., for the logic L-3.

关键词： first order logic counting quantifiers quantifier depth Weisfeiler-Leman

来源：评论

学校读者我要写书评

暂无评论

Test-point insertion efficiency analysis for LBIST applications 34

Test-point insertion efficiency analysis for LBIST applicati...

引用

34th ieee VLSI Test symposium, VTS 2016

作者： He, Miao Tony Contreras, Gustavo K. Tehranipoor, Mark Tran, Dat Winemberg, LeRoy Department of Electrical and Computer Engineering University of Florida GainesvilleFL32611 United States NXP Semiconductors AustinTX78735 United States

ISBN: (纸本)9781467384544

Test points are inserted into integrated circuits to increase fault coverage especially in logic built-in self-test (LBIST) schemes. Commercial tools have been developed over the past decade to insert test points in circuits under test, but they are often inefficient and incur unacceptably large area overhead. Our analysis shows that many test points have little or no impact on test coverage. therefore, we propose a framework to evaluate test point's impact on a design and rank them based on their efficiency, and to obtain an optimal configuration of the most efficient test points accurately and rapidly. Within this framework, we have two metrics;namely the efficient test point insertion (ETPI) metric and the test point removal estimation (TPRE) metric. the ETPI metric is developed to remove the most inefficient test points inserted in the circuits by the commercial tools, thereby minimizing area penalty with very limited test coverage loss. the TPRE metric is introduced to quickly select the appropriate test point removal scheme. Since TPRE can estimate area overhead and test coverage for designs with different percentage of test points removed without the actual insertion of test points and without the need for lengthy circuit simulation, large amount of processing time is saved especially for large circuits. Experimental results indicate that ETPI can reduce area overhead reduction by up to 95.00% with test coverage reduction as low as 0.57%. In addition, results by applying the TPRE metric indicate that the difference between estimation and actual simulation/synthesis results for area overhead is less than 0.10% for most cases, and the difference between them for test coverage is less than 1.00% for most cases. © 2016 ieee.

关键词： Built-in self test

来源：评论

学校读者我要写书评

暂无评论

proceedings - 2013 28th annual acm/ieee symposium on logic in computer science, LICS 2013

Proceedings - 2013 28th Annual ACM/IEEE Symposium on Logic i...

引用

2013 28th annual acm/ieee symposium on logic in computer science, LICS 2013

the proceedings contain 59 papers. the topics discussed include: from qualitative to quantitative proofs of security properties using first-order conditional logic;regular functions and cost register automata;reasoning about data repetitions with counter systems;on the context-freeness problem for vector addition systems;an optimal Gaifman normal form construction for structures of bounded degree;topological structure of quantum algorithms;on the query complexity of real functionals;magnitude monadic logic over words and the use of relative internal set theory;model checking for successor-invariant first-order logic on minor-closed graph classes;dynamic logic of propositional assignments: a well-behaved variant of PDL;the complexity of model checking multi-stack systems;maximum matching and linear programming in fixed-point logic with counting;and adding an equivalence relation to the interval logic ABB: complexity and expressiveness.

关键词：

来源：评论

学校读者我要写书评

暂无评论

proceedings - symposium on logic in computer science

Proceedings - Symposium on Logic in Computer Science

引用

30th annual acm/ieee symposium on logic in computer science, LICS 2015

ISBN: (纸本)9781479988754

the proceedings contain 66 papers. the topics discussed include: reachability in two-dimensional vector addition systems with states is PSPACE-complete;demystifying reachability in vector addition systems;complexity bounds for sum-product logic via additive proof nets and Petri nets;multidimensional beyond worst-case and almost-sure problems for mean-payoff objectives;improved algorithms for one-pair and k-pair Streett objectives;the hunt for a red spider: conjunctive query determinacy is undecidable;the complexity of boundedness for guarded logics;tree-like queries in OWL 2 QL: succinctness and complexity results;path logics for querying graphs: combining expressiveness and efficiency;monadic second-order logic and bisimulation invariance for coalgebras;defining winning strategies in fixed-point logic;from complexity to algebra and back: digraph classes, collapsibility, and the PGP;and descriptive complexity of list H-coloring problems in Logspace: a refined dichotomy.

关键词：

来源：评论

学校读者我要写书评

暂无评论

Parka: thermally insulated nanophotonic interconnects 15

Parka: Thermally insulated nanophotonic interconnects

引用

9th ieee/acm International symposium on Networks-on-Chip, NOCS 2015

作者： Demir, Yigit Hardavellas, Nikos Northwestern University Department of Electrical Engineering and Computer Science EvanstonIL United States

ISBN: (纸本)9781450333962

Silicon-photonics are emerging as the prime candidate technology for energy-efficient on-chip interconnects at future process nodes. However, current designs are primarily based on microrings, which are highly sensitive to temperature. As a result, current silicon-photonic interconnect designs expend a significant amount of energy heating the microrings to a designated narrow temperature range, only to have the majority of the thermal energy waste away and dissipate through the heat sink, and in the process of doing so heat up the logic layer, causing significant performance degradation to the cores and inducing thermal emergencies. We propose Parka, a nanophotonic interconnect that encases the photonic die in a thermal insulator that keeps its temperature stable with low energy expenditure, while minimizing the spatial and temporal thermal coupling between logic and silicon-photonic components. Parka reduces the microring energy by 3.8-5.4x and achieves 11-23% speedup on average (34% max) depending on the cooling solution used. Copyright is held by the owner/author(s).

关键词： Silicon photonics

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：