Previsão de desvios em arquiteturas multitarefas simultâneas

A exploração do paralelismo no nível de instrução (ILP) em arquiteturas superescalares é limitada fortemente pelas dependências de controle, as quais são ocasionadas pelas instruções de desvio, e pelas dependências de dados. As arquiteturas SMT (Simultaneous MultiThreaded) buscam explorar um novo nível de paralelismo, denominado paralelismo no nível de tarefa (TLP), para buscar e executar instruções de diversas tarefas ao mesmo tempo. Com isso, enquanto uma tarefa está bloqueada por dependências de controle e de dados, outras tarefas podem continuar executando, mascarando assim as latências de previsões incorretas e de acessos à memória, usando mais eficientemente as unidades funcionais e demais recursos disponíveis. Contudo, o projeto dessas arquiteturas continua a esbarrar nos mesmos problemas associados ao uso de técnicas utilizadas para a exploração de ILP, como a previsão de devios. Além disso, essas arquiteturas trazem novos desafios, como a determinação da maneira mais eficiente de distribuição/compartilhamento de recursos entre as tarefas. Nesse trabalho será apresentada uma topologia para as tabelas de previsão de desvios em arquiteturas multitarefas simultâneas. Além disso, serão desenvolvidas duas análises complementares acerca de previsão de desvios: o impacto da taxa de acertos da previsão de desvios em arquiteturas com pipelines profundos e o impacto da taxa de acerto na previsão do alvo de um desvio. Entre as principais contribuições do trabalho pode-se citar a definição de uma estrutura particionada para as tabelas de previsão em arquiteturas SMT, aliando desempenho a um menor custo de implementação em uma arquitetura real. Além disso, é mostrado que a taxa de acerto da previsão de desvios tem um grande impacto no desempenho das arquiteturas SMT com pipelines profundos, bem como nas causas de bloqueio do estágio de busca quando utiliza-se cache de instruções bloqueantes.

Prova automática de satisfatibilidade módulo teoria aplicada ao método B

Este trabalho apresenta uma extensão do provador haRVey destinada à verificação de obrigações de prova originadas de acordo com o método B. O método B de desenvolvimento de software abrange as fases de especificação, projeto e implementação do ciclo de vida do software. No contexto da verificação, destacam-se as ferramentas de prova Prioni, Z/EVES e Atelier-B/Click n Prove. Elas descrevem formalismos com suporte à checagem satisfatibilidade de fórmulas da teoria axiomática dos conjuntos, ou seja, podem ser aplicadas ao método B. A checagem de SMT consiste na checagem de satisfatibilidade de fórmulas da lógica de primeira-ordem livre de quantificadores dada uma teoria decidível. A abordagem de checagem de SMT implementada pelo provador automático de teoremas haRVey é apresentada, adotando-se a teoria dos vetores que não permite expressar todas as construções necessárias às especificações baseadas em conjuntos. Assim, para estender a checagem de SMT para teorias dos conjuntos destacam-se as teorias dos conjuntos de Zermelo-Frankel (ZFC) e de von Neumann-Bernays-Gödel (NBG). Tendo em vista que a abordagem de checagem de SMT implementada no haRVey requer uma teoria finita e pode ser estendida para as teorias nãodecidíveis, a teoria NBG apresenta-se como uma opção adequada para a expansão da capacidade dedutiva do haRVey à teoria dos conjuntos. Assim, através do mapeamento dos operadores de conjunto fornecidos pela linguagem B a classes da teoria NBG, obtem-se uma abordagem alternativa para a checagem de SMT aplicada ao método B

Deciding difference logic in a Nelson-Oppen combination framework

O método de combinação de Nelson-Oppen permite que vários procedimentos de decisão, cada um projetado para uma teoria específica, possam ser combinados para inferir sobre teorias mais abrangentes, através do princípio de propagação de igualdades. Provadores de teorema baseados neste modelo são beneficiados por sua característica modular e podem evoluir mais facilmente, incrementalmente. Difference logic é uma subteoria da aritmética linear. Ela é formada por constraints do tipo x − y ≤ c, onde x e y são variáveis e c é uma constante. Difference logic é muito comum em vários problemas, como circuitos digitais, agendamento, sistemas temporais, etc. e se apresenta predominante em vários outros casos. Difference logic ainda se caracteriza por ser modelada usando teoria dos grafos. Isto permite que vários algoritmos eficientes e conhecidos da teoria de grafos possam ser utilizados. Um procedimento de decisão para difference logic é capaz de induzir sobre milhares de constraints. Um procedimento de decisão para a teoria de difference logic tem como objetivo principal informar se um conjunto de constraints de difference logic é satisfatível (as variáveis podem assumir valores que tornam o conjunto consistente) ou não. Além disso, para funcionar em um modelo de combinação baseado em Nelson-Oppen, o procedimento de decisão precisa ter outras funcionalidades, como geração de igualdade de variáveis, prova de inconsistência, premissas, etc. Este trabalho apresenta um procedimento de decisão para a teoria de difference logic dentro de uma arquitetura baseada no método de combinação de Nelson-Oppen. O trabalho foi realizado integrando-se ao provador haRVey, de onde foi possível observar o seu funcionamento. Detalhes de implementação e testes experimentais são relatados

Search for the flavor-changing neutral current decay Bs 0 → μ+ μ- pp̄ Collisions at √s = 1.96 TeV with the DO Detector

We present the results of a search for the flavor-changing neutral current decay Bs 0 → μ+ μ-. using a data set with integrated luminosity of 240 pb-1 of pp̄ collisions at √s = 1.96 TeV collected with the D0 detector in run II of the Fermilab Tevatron collider. We find the upper limit on the branching fraction to be B(Bs 0 → μ+ π-) ≤ 5.0 × 10-7 at the 95% C.L. assuming no contributions from the decay Bd 0 → μ+ μ- in the signal region. This limit is the most stringent upper bound on the branching fraction Bs 0 → μ+ μ- to date. © 2005 The American Physical Society.

Simplified computational routine to correct the modal decoupling in transmission lines and power systems modelling

Modal analysis is widely approached in the classic theory of power systems modelling. This technique is also applied to model multiconductor transmission lines and their self and mutual electrical parameters. However, this methodology has some particularities and inaccuracies for specific applications, which are not clearly described in the technical literature. This study provides a brief review on modal decoupling applied in transmission line digital models and thereafter a novel and simplified computational routine is proposed to overcome the possible errors embedded by the modal decoupling in the simulation/ modelling computational algorithm. © The Institution of Engineering and Technology 2013.

Propriedades analíticas de materiais a base de sílica e óxido de titânio modificados

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Malungos do sertão: cotidiano, práticas mágicas e feitiçaria no Mato Grosso setecentista

Coordenação de Aperfeiçoamento de Pessoal de Nível Superior (CAPES)

Simplified skin-effect formulation for power transmission lines

Fundação de Amparo à Pesquisa do Estado de São Paulo (FAPESP)

Effects of melatonin on ovarian follicles

Objective: To evaluate the histomorphometry and expression of Ki-67 and c-kit in ovarian follicles of pinealectomized or melatonin-treated pinealectomized rats. Study design: Forty adult rats were randomly divided into four groups of 10 animals: Group I – control; Group II – sham-pinealectomized; Group III – pinealectomized (Px), and Group IV – Px treated with melatonin (10 mg/night, per animal). After two months’ treatment, on the night of proestrous, the animals were placed in metabolic cages for night urine collection and subsequent measurement of 6-sulfatoxymelatonin (6-SMT). The rats were anesthetized, blood samples were taken for estrogen and progesterone determinations, and they were then euthanized. The ovaries were dissected out for further histological and immunohistochemical analyses. Data were first submitted to analysis of variance (ANOVA) complemented with the Tukey–Kramer test for multiple comparisons (P < 0.05). Results: The urinary levels of 6-SMT and serum progesterone were lower in the Px group (GIII). Exogenous melatonin treatment restored both blood melatonin and 6-SMT urinary levels. The histomorphometric data in Group III revealed a significant increase of degenerating antral and nonantral follicles with regard to the other groups. In addition no corpora lutea were observed in this group. No significant differences were noticed regarding the number of corpora lutea among the other groups (I, II and IV), but the number of cells and the thickness of the theca interna of Px animals (Group III) were higher than in the other groups. Conversely, the density of progesterone receptors (fmol/g) in the ovaries of Group III was significantly lower than in the other groups. Conclusion: Our data indicate that melatonin exerts a role on the maintenance of a proper follicular function, and is thus important for ovulation and progesterone production.

Impiego della spettrometria di massa nell'analisi di fumonisine in alimenti e matrici di origine animale

Mycotoxins are heterogeneous chemical compounds characterized by a low molecular weight and synthesized by the secondary metabolism of different molds. Fumonisins are water-soluble mycotoxins produced by Fusarium species spoiling corn and derived produc ts. These mycotoxins can be a health hazard when consuming contaminated cereals, but they can reach humans also indirectly through the consumption of food products derived from animals fed with contaminated feed. Fumonisins have been associated with several animal and human diseases: they are suspected risk factors for esophageal and liver cancers, neural tube defects and cardiovascular problems. Improved methods are needed to accurately assess fumonisins concentrations in food of vegetable and animal origin, in order to prevent acute and chronic human exposure. The aim of the present work was to evaluate the versatility and the performances of mass spectrometry, coupled with liquid chromatography, in fumonisins analysis from foods and matrices of animal origin. Different methods for the identification and quantification of fumonisins and related products have been developed and validated to determine fumonisin B1 in milk, fumonisin B1, fumonisin B2 and their complete hydrolyzed products (HFB1 and HFB2) in pig liver and fumonisins B1 and B2 in complete and complementary dry dog food. The experimental procedures have been carefully studied, considering matrices features, number and type of molecules to detect. Therefore, several extraction, clean up and separation techniques were tested in order to obtain the better conditions of sample processing. The fit for purpose sample preparation, matched with high mass spectrometry sensibility and specificity, have allowed to achieve good results in any tested animal matrices. Hence, the developed methods were validated and have shown a high accuracy, sensibility and precision, fulfilling performance requirements of Decision 2002/657/EC and of European Project Standard, Measuring and Testing (SMT). In any developed method, the analytes were identified and quantified even at very low concentrations : the limits of quantification resulted lower than other similar works, performed with different detectors. These methods were applied to some commercial samples and to some samples collected for research projects in the Department of Veterinary Public Health and Animal Pathology (DVPHAP) of University of Bologna. Although the disclosed data must be considered completely preliminary and without statistical significance, they emphasize the presence of mycotoxins in animal products. The outcomes obtained from the processed samples (bovine milk, pig liver and dry dog food) suggest the efficacy of these methods also on other food matrices, confirming the versatility and the performances of mass spectrometry, coupled with liquid chromatography, in fumonisins analysis. Moreover the results underline the need to set up a large scale monitoring in order to evaluate the presence of fumonisins in food of animal origin for human consumption.

Efficient certification of feasibility and objective value of linear programs and its applications

The use of linear programming in various areas has increased with the significant improvement of specialized solvers. Linear programs are used as such to model practical problems, or as subroutines in algorithms such as formal proofs or branch-and-cut frameworks. In many situations a certified answer is needed, for example the guarantee that the linear program is feasible or infeasible, or a provably safe bound on its objective value. Most of the available solvers work with floating-point arithmetic and are thus subject to its shortcomings such as rounding errors or underflow, therefore they can deliver incorrect answers. While adequate for some applications, this is unacceptable for critical applications like flight controlling or nuclear plant management due to the potential catastrophic consequences. We propose a method that gives a certified answer whether a linear program is feasible or infeasible, or returns unknown'. The advantage of our method is that it is reasonably fast and rarely answers unknown'. It works by computing a safe solution that is in some way the best possible in the relative interior of the feasible set. To certify the relative interior, we employ exact arithmetic, whose use is nevertheless limited in general to critical places, allowing us to rnremain computationally efficient. Moreover, when certain conditions are fulfilled, our method is able to deliver a provable bound on the objective value of the linear program. We test our algorithm on typical benchmark sets and obtain higher rates of success compared to previous approaches for this problem, while keeping the running times acceptably small. The computed objective value bounds are in most of the cases very close to the known exact objective values. We prove the usability of the method we developed by additionally employing a variant of it in a different scenario, namely to improve the results of a Satisfiability Modulo Theories solver. Our method is used as a black box in the nodes of a branch-and-bound tree to implement conflict learning based on the certificate of infeasibility for linear programs consisting of subsets of linear constraints. The generated conflict clauses are in general small and give good rnprospects for reducing the search space. Compared to other methods we obtain significant improvements in the running time, especially on the large instances.

The Making of a Shiite Bourgeoisie in Lebanon Political Mobilisation, Economic Resources and Formation of a Social Group

The thesis analyses the making of the Shiite middle- and upper/entrepreneurial-class in Lebanon from the 1960s till the present day. The trajectory explores the historical, political and social (internal and external) factors that brought a sub-proletariat to mobilise and become an entrepreneurial bourgeoisie in the span of less than three generations. This work proposes the main theoretical hypothesis to unpack and reveal the trajectory of a very recent social class that through education, diaspora, political and social mobilisation evolved in a few years into a very peculiar bourgeoisie: whereas Christian-Maronite middle class practically produced political formations and benefited from them and from Maronite’s state supremacy (National Pact, 1943) reinforcing the community’s status quo, Shiites built their own bourgeoisie from within, and mobilised their “cadres” (Boltanski) not just to benefit from their renovated presence at the state level, but to oppose to it. The general Social Movement Theory (SMT), as well as a vast amount of the literature on (middle) class formation are therefore largely contradicted, opening up new territories for discussion on how to build a bourgeoisie without the state’s support (Social Mobilisation Theory, Resource Mobilisation Theory) and if, eventually, the middle class always produces democratic movements (the emergence of a social group out of backwardness and isolation into near dominance of a political order). The middle/upper class described here is at once an economic class related to the control of multiple forms of capital, and produced by local, national, and transnational networks related to flows of services, money, and education, and a culturally constructed social location and identity structured by economic as well as other forms of capital in relation to other groups in Lebanon.

Development of Solid Oxide Fuel Cell Electrodes with High Conductivity and Enhanced Redox Stability

The intent of this study was the development of new ceramic SOFC anode materials which possess electrical conductivity as well as redox stability.

A randomised controlled trial of spinal manipulative therapy in acute low back pain

OBJECTIVE: To determine whether treatment with spinal manipulative therapy (SMT) administered in addition to standard care is associated with clinically relevant early reductions in pain and analgesic consumption. METHODS: 104 patients with acute low back pain were randomly assigned to SMT in addition to standard care (n = 52) or standard care alone (n = 52). Standard care consisted of general advice and paracetamol, diclofenac or dihydrocodeine as required. Other analgesic drugs or non-pharmacological treatments were not allowed. Primary outcomes were pain intensity assessed on the 11-point box scale (BS-11) and analgesic use based on diclofenac equivalence doses during days 1-14. An extended follow-up was performed at 6 months. RESULTS: Pain reductions were similar in experimental and control groups, with the lower limit of the 95% CI excluding a relevant benefit of SMT (difference 0.5 on the BS-11, 95% CI -0.2 to 1.2, p = 0.13). Analgesic consumptions were also similar (difference -18 mg diclofenac equivalents, 95% CI -43 mg to 7 mg, p = 0.17), with small initial differences diminishing over time. There were no differences between groups in any of the secondary outcomes and stratified analyses provided no evidence for potential benefits of SMT in specific patient groups. The extended follow-up showed similar patterns. CONCLUSIONS: SMT is unlikely to result in relevant early pain reduction in patients with acute low back pain.