Les compilateurs modernes constituent des programmes complexes, réalisant de nombreuses optimisations afin d'améliorer la performance du code généré. Du fait de cette complexité, des bugs y sont régulièrement détecté, conduisant à l'introduction de nouveau comportement dans le programme compilé. En réaction, il est aujourd'hui possible de prouver correct, dans des assistants de preuve tels que Coq, des compilateurs optimisants pour des langages tels que le C ou ML. Transporter un tel résultat pour des langages haut-niveau tels que Java est néanmoins encore hors de portée de l'état de l'art. Ceux-ci possèdent en effet deux caractéristiques essentielles: la concurrence et un environnement d'exécution particulièrement complexe.Nous proposons dans cette thèse de réduire la distance vers la conception d'un tel compilateur vérifié en nous concentrant plus spécifiquement sur la preuve de correction d'un glaneur de cellules concurrent performant. Ce composant de l'environnement d'exécution prend soin de collecter de manière automatique la mémoire, en lieu et place du programmeur. Afin de ne pas générer un ralentissement trop élevé à l'exécution, le glaneur de cellules doit être extrêmement performant. Plus spécifiquement, l'algorithme considéré est dit «au vol»: grâce à l'usage de concurrence très fine, il ne cause jamais d'attente active au sein d'un fil utilisateur. La preuve de correction établit par conséquent que malgré l'intrication complexe des fils utilisateurs et du collecteur, ce dernier ne collecte jamais une cellule encore accessible par les premiers. Nous présentons dans un premier temps l'algorithme considéré et sa formalisation en Coq dans une représentation intermédiaire conçue pour l'occasion. Nous introduisons le système de preuve que nous avons employé, une variante issue de la logique «Rely-Guarantee», et prouvons l'algorithme correct. Raisonner simultanément sur l'algorithme de collection et sur l'implantation des structures de données concurrentes manipulées générerait une complexité additionnelle indésirable. Nous considérons donc durant la preuve des opérations abstraites: elles ont lieu instantanément. Pour légitimer cette simplification, nous introduisons une méthode inspirée par les travaux de Vafeiadis et permettant la preuve de raffinement de structures de données concurrentes dites «linéarisables». Nous formalisons l'approche en Coq et la dotons de solides fondations sémantiques. Cette méthode est finalement instanciée sur la principale structure de données utilisée par le glaneur de cellules. / Modern compilers are complex programs, performing several heuristic-based optimisations. As such, and despite extensive testing, they may contain bugs leading to the introduction of new behaviours in the compiled program.To address this issue, we are nowadays able to prove correct, in proof assistants such as Coq, optimising compilers for languages such as C or ML. To date, a similar result for high-level languages such as Java nonetheless remain out of reach. Such languages indeed possess two essential characteristics: concurrency and a particularly complex runtime.This thesis aims at reducing the gap toward the implementation of such a verified compiler. To do so, we focus more specifically on a state-of-the-art concurrent garbage collector. This component of the runtime takes care of automatically reclaiming memory during the execution to remove this burden from the developer side. In order to keep the induced overhead as low as possible, the garbage collector needs to be extremely efficient. More specifically, the algorithm considered is said to be ``on the fly'': by relying on fine-grained concurrency, the user-threads are never caused to actively wait. The key property we establish is the functional correctness of this garbage collector, i.e. that a cell that a user thread may still access is never reclaimed.We present in a first phase the algorithm considered and its formalisation in Coq by implementing it in a dedicated intermediate representation. We introduce the proof system we used to conduct the proof, a variant based on the well-established Rely-Guarantee logic, and prove the algorithm correct.Reasoning simultaneously over both the garbage collection algorithm itself and the implementation of the concurrent data-structures it uses would entail an undesired additional complexity. The proof is therefore conducted with respect to abstract operations: they take place instantaneously. To justify this simplification, we introduce in a second phase a methodology inspired by the work of Vafeiadis and dedicated to the proof of observational refinement for so-called ``linearisable'' concurrent data-structures. We provide the approach with solid semantic foundations, formalised in Coq. This methodology is instantiated to soundly implement the main data-structure used in our garbage collector.

Submitted by JOÃO VITOR RAMOS DA SILVA null (joaopontogeo@gmail.com) on 2016-04-15T01:58:52Z No. of bitstreams: 1 Dissertação João - Versão Final Biblioteca.pdf: 5062608 bytes, checksum: d13064d87e2458bae58a8c4ac9fb649d (MD5) / Rejected by Felipe Augusto Arakaki (arakaki@reitoria.unesp.br), reason: Solicitamos que realize uma nova submissão seguindo as orientações abaixo: O arquivo submetido está sem a ficha catalográfica. A versão submetida por você é considerada a versão final da dissertação/tese, portanto não poderá ocorrer qualquer alteração em seu conteúdo após a aprovação. Corrija esta informação e realize uma nova submissão contendo o arquivo correto. Agradecemos a compreensão. on 2016-04-18T17:48:11Z (GMT) / Submitted by JOÃO VITOR RAMOS DA SILVA null (joaopontogeo@gmail.com) on 2016-04-18T21:59:36Z No. of bitstreams: 1 Dissertação João - Versão Final Biblioteca.pdf: 5070849 bytes, checksum: f6648ed4572f687dbc0b9e763b803e17 (MD5) / Approved for entry into archive by Felipe Augusto Arakaki (arakaki@reitoria.unesp.br) on 2016-04-19T13:50:23Z (GMT) No. of bitstreams: 1 silva_jvr_me_prud.pdf: 5070849 bytes, checksum: f6648ed4572f687dbc0b9e763b803e17 (MD5) / Made available in DSpace on 2016-04-19T13:50:23Z (GMT). No. of bitstreams: 1 silva_jvr_me_prud.pdf: 5070849 bytes, checksum: f6648ed4572f687dbc0b9e763b803e17 (MD5) Previous issue date: 2016-03-18 / Conselho Nacional de Desenvolvimento Científico e Tecnológico (CNPq) / Esta dissertação se refere ao trabalho situado “por detrás das lixeiras da sociedade”, protagonizado pelos coletores de lixo domiciliar urbano na cidade de Presidente Prudente/SP. Buscou-se evidenciar as rotinas e processos de trabalho desses sujeitos, identificando as consequências para sua saúde e de que forma o fenômeno da invisibilidade social ocorre no contexto laboral da coleta de lixo. A pesquisa incluiu levantamento bibliográfico voltado a três eixos-mestres – trabalho na coleta de lixo, saúde do trabalhador e invisibilidade social –, realização de entrevistas semiestruturadas com os sujeitos e agentes da pesquisa (coletores, sindicalista e representante do Ministério Público do Trabalho) e uso de informações secundárias de diversas fontes. Esse conjunto compôs as ferramentas analíticas empregadas para construir um enredo capaz de dar voz aos coletores de lixo. O trabalho na coleta é extremamente penoso e gera efeitos nocivos à saúde dos trabalhadores, em curto e principalmente em longo prazo, quando as dores no corpo tornam-se crônicas. Ademais, a invisibilidade social e a concomitante humilhação contribuem para precariedade laboral em termos da saúde mental dos coletores. Observa-se fragilidade na luta sindical no que tange a remuneração e aumentos salariais, e na própria relação com os coletores, embora haja algumas conquistas pontuais, como a obtenção e incremento de equipamentos de proteção individual. A insatisfação dos coletores com sua representação sindical frente à empresa empregadora, todavia, não é suficiente para ensejar uma articulação concreta entre os próprios trabalhadores, pelo temor de represálias ou da perda do emprego. / This paper refers to the labor located “behind the bins of society” experienced by urban garbage collectors in the city of Presidente Prudente (State of São Paulo, Brazil). It sought to highlight the routines and work processes of these individuals, identifying the consequences for their health and how the phenomenon of social invisibility occurs in the labor context of garbage collection. The research included literature review focused on three master-axes (work in garbage collection, workers‟ health and social invisibility), semi-structured interviews with the subjects and agents of the survey (collectors, union leader and representative of the Ministry of Labor) and using secondary information from various sources. This set composed the analytical tools used to build a storyline capable of giving voice to garbage collectors. Garbage collection is burdensome and generates harmful effects on workers‟ health, in short term and mainly in long term, when body pains become chronic. Moreover, the social invisibility and concomitant humiliation contribute to labor precariousness in terms of collectors‟ mental health. It is observed weakness in the trade union efforts concerning to remuneration and salary increases, as well as in the relation with the collectors, although there are some specific achievements like getting and incrementing personal protective equipment. The collectors‟ dissatisfaction with their union representation against the employer company, however, is not sufficient to bring a concrete coordination between the workers themselves, because of fear of reprisals or job loss. / CNPq: 130639/2013-3

O objetivo desta dissertação foi mostrar o cenário atual e as perspectivas para o setor de saneamento básico do Estado de Roraima. Destacou-se o perfil dos serviços de abastecimento de água, coleta de esgotos e coleta de lixo. Foram utilizadas diversas publicações, especialmente as do Instituto Brasileiro de Geografia e Estatística/IBGE, com destaque para a Pesquisa Nacional por Amostra de Domicílios/PNAD e o Censo Demográfico 2000, que forneceram dados da população urbana do Estado atendida e não atendida pelos serviços de saneamento básico. Dessa forma, foi realizada a comparação dos resultados obtidos para o Estado com algumas cidades brasileiras, regiões do país, além de outros países. Sob esse aspecto, os resultados apurados apontaram que 96,9% dos domicílios urbanos do Estado, são atendidos pelos serviços de abastecimento de água, superando a realidade nacional. Quanto à coleta de esgotos, os resultados são preocupantes, uma vez que apenas 17,3% dos domicílios urbanos do Estado são atendidos por este serviço. Já a coleta de lixo 97,1% dos domicílios urbanos do Estado possui acesso a esse serviço. Constatou-se, ainda, que a maior parte do lixo coletado no Estado de Roraima é depositada a céu aberto, sem nenhum tratamento quanto às questões ambientais. Concluiu-se que a população urbana do Estado de Roraima apresenta ótimos resultados quanto ao acesso aos serviços de abastecimento de água e coleta de lixo. Contudo, a mesma situação não é observada quanto ao acesso aos serviços de coleta de esgotos, onde uma pequena parcela da população urbana é atendida. Nesse sentido, já existem recursos disponíveis para a universalização dos serviços de abastecimento de água e ampliação do sistema de esgoto sanitário. Entretanto, os recursos destinados a ampliação do sistema de esgotos ainda não é suficiente para atender a toda a população. / The objective of this thesis was to show the current scenario and prospects for the basic sanitation sector in the State of Roraima, showing the profile of the following services: water supply, waste sewage disposal and garbage collection. To obtain the data, various publications were used , especially the Brazilian Institute of Geography and Statistics (IBGE), highlighting the National Survey of Home Sampling (PNAD) and the year 2000 Census which provided data on the urban population of the state with and without sanitation services. Thus, the results for the state were compared with other Brazilian cities, regions of the country and other countries. The findings indicate that 96.9% of urban households in the state are served by the water supply, surpassing the national reality, while the sewage disposal results are worrisome as only 17.3% of urban households in the state are served. As for garbage collection, 97.1% of urban households of the state have access to this service. It was further observed that most of the garbage collected in the state of Roraima is deposited in the open, without any form of treatment for environmental concerns. It was concluded that the urban population of the state of Roraima in great part have access to services of water supply and garbage collection. However, the same was not observed for sewage disposal services, where only a small portion of the urban population is served. There are resources available for expanding the water supply to service more households and the expansion of the sewerage system. However, the resources allocated for the expansion of sewerage system is not sufficient to meet the demands of the entire state population, and so, the need for a larger volume of investment.

O objetivo desta dissertação foi mostrar o cenário atual e as perspectivas para o setor de saneamento básico do Estado de Roraima. Destacou-se o perfil dos serviços de abastecimento de água, coleta de esgotos e coleta de lixo. Foram utilizadas diversas publicações, especialmente as do Instituto Brasileiro de Geografia e Estatística/IBGE, com destaque para a Pesquisa Nacional por Amostra de Domicílios/PNAD e o Censo Demográfico 2000, que forneceram dados da população urbana do Estado atendida e não atendida pelos serviços de saneamento básico. Dessa forma, foi realizada a comparação dos resultados obtidos para o Estado com algumas cidades brasileiras, regiões do país, além de outros países. Sob esse aspecto, os resultados apurados apontaram que 96,9% dos domicílios urbanos do Estado, são atendidos pelos serviços de abastecimento de água, superando a realidade nacional. Quanto à coleta de esgotos, os resultados são preocupantes, uma vez que apenas 17,3% dos domicílios urbanos do Estado são atendidos por este serviço. Já a coleta de lixo 97,1% dos domicílios urbanos do Estado possui acesso a esse serviço. Constatou-se, ainda, que a maior parte do lixo coletado no Estado de Roraima é depositada a céu aberto, sem nenhum tratamento quanto às questões ambientais. Concluiu-se que a população urbana do Estado de Roraima apresenta ótimos resultados quanto ao acesso aos serviços de abastecimento de água e coleta de lixo. Contudo, a mesma situação não é observada quanto ao acesso aos serviços de coleta de esgotos, onde uma pequena parcela da população urbana é atendida. Nesse sentido, já existem recursos disponíveis para a universalização dos serviços de abastecimento de água e ampliação do sistema de esgoto sanitário. Entretanto, os recursos destinados a ampliação do sistema de esgotos ainda não é suficiente para atender a toda a população. / The objective of this thesis was to show the current scenario and prospects for the basic sanitation sector in the State of Roraima, showing the profile of the following services: water supply, waste sewage disposal and garbage collection. To obtain the data, various publications were used , especially the Brazilian Institute of Geography and Statistics (IBGE), highlighting the National Survey of Home Sampling (PNAD) and the year 2000 Census which provided data on the urban population of the state with and without sanitation services. Thus, the results for the state were compared with other Brazilian cities, regions of the country and other countries. The findings indicate that 96.9% of urban households in the state are served by the water supply, surpassing the national reality, while the sewage disposal results are worrisome as only 17.3% of urban households in the state are served. As for garbage collection, 97.1% of urban households of the state have access to this service. It was further observed that most of the garbage collected in the state of Roraima is deposited in the open, without any form of treatment for environmental concerns. It was concluded that the urban population of the state of Roraima in great part have access to services of water supply and garbage collection. However, the same was not observed for sewage disposal services, where only a small portion of the urban population is served. There are resources available for expanding the water supply to service more households and the expansion of the sewerage system. However, the resources allocated for the expansion of sewerage system is not sufficient to meet the demands of the entire state population, and so, the need for a larger volume of investment.

This report evaluates whether an interpreted high-level garbage collected language has enough information about its memory behaviour to make better cache decisions than modern general CPU hardware. With a generational garbage collector, depending on promotion algorithm and generation size, around 90% of all objects never leave the first generation. This report is based on the hypothesis that, because of the low promotion rate, accesses to higher generations are sufficiently rare not to benefit from caching. To test this hypothesis, we built an operating system with a Scheme interpreter in kernel mode, where the interpreter controls the cache. Generic x86 PC hardware was used, since it allows fine-grained control of cache decisions. Measurements of execution time in this interpreter show that disabling the cache for generations higher than the first does not give any performance gain, but rather a performance loss of up to 50%. We conclude that this interpreter design is not an improvement, but cannot conclude that the hypothesis is false in general. We suggest building a better CPU simulator to gather more data from which to make better caching decisions, moving internal interpreter data structures into the garbage collected heap and modifying the hardware to allow control in the currently rigid dimension of where data is cached---for example separate control of instruction and data caches and separate data caches for different areas of memory.

With increasing clock-rates in CPUs coming to an end, a need for parallelization has emerged. This thesis proposes a dynamic purity analysis of objects, detecting independent execution paths that may be run in parallel. The analysis relies in speculative guesses and may be rolled back when proven wrong. It piggybags on an efficient replicating garbage collector integrated to JVM. The efficiency of the algorithms are shown in benchmark, and are comparable to the speed of state of the art garbage collectors in hotspot’s JVM. With this dynamic purity analysis now accessible in Java programs, the potential for automatic JIT-parallelization of pure methods is possible.

This report details the design of a garbage collection (GC) module, which introduces modern GC features to the domain of embedded implementations. The described design supports weak references and feeds reference queues. Its architecture allows multiple concurrent application cores operating as mutators on the shared memory managed by the GC module. The garbage collection is exact and fully concurrent so as to enable the uninterrupted computational progress of the mutators. It combines a distributed root marking with a centralized heap scan of the managed memory. It features a novel mark-and-copy GC strategy on a segmented memory, which thereby overcomes both the tremendous space overhead of two-space copying and the compaction race of mark-and-compact approaches. The proposed GC architecture has been practically implemented and proven using the embedded bytecode processor SHAP as a sample testbed. The synthesis results for settings up to three SHAP mutator cores are given and online functional measurements are presented. Basic performance dependencies on the system configuration are evaluated.

Purely functional languages--with static type systems and dynamic memory management using garbage collection--are a known tool for helping programmers to reduce the number of memory errors in programs. By using such languages, we can establish correctness properties relating to memory-safety through our choice of implementation language alone. Unfortunately, the language characteristics that make purely functional languages safe also make them more difficult to apply in a low-level domain like operating systems construction. The low-level features that support the kinds of hardware manipulations required by operating systems are not typically available in memory-safe languages with garbage collection. Those that are provided may have the ability to violate memory- and type-safety, destroying the guarantees that motivate using such languages in the first place. This work demonstrates that it is possible to bridge the gap between the requirements of operating system implementations and the features of purely functional languages without sacrificing type- and memory-safety. In particular, we show that this can be achieved by isolating the potentially unsafe memory operations required by operating systems in an abstraction layer that is well integrated with a purely functional language. The salient features of this abstraction layer are that the operations it exposes are memory-safe and yet sufficiently expressive to support the implementation of realistic operating systems. The abstraction layer enables systems programmers to perform all of the low-level tasks necessary in an OS implementation, such as manipulating an MMU and executing user-level programs, without compromising the static memory-safety guarantees of programming in a purely functional language. A specific contribution of this work is an analysis of memory-safety for the abstraction layer by formalizing a meaning for memory-safety in the presence of virtual-memory using a novel application of noninterference security policies. In addition, we evaluate the expressiveness of the abstraction layer by implementing the L4 microkernel API, which has a flexible set of virtual memory management operations.

Denna rapport jämför prestanda med Unitys nya inkrementella garbage collection system med deras tidigare stop the world system, samt analyserar effekten av objektpooling på tidsprestanda. De olika systemen testas med hjälp av en förenklad version av ett bullet hell spel, där flertalet kulor skapas och förstörs per sekund. Rapporten finner att användning av objektpooling drastiskt förbättrar prestanda i den givna testmiljön. Rapporten finner även att stop the world presterar något bättre i genomsnitt, men dess extremvärden är markant högre på grund av garbage collection spikar. Rapporten rekommenderar användning av pooling samt användning av det inkrementella garbage collection systemet för att minimera överskridande av spelets tidsbudget per bilduppdatering.

No description available.