All Projects → johnwickerson → memalloy

johnwickerson / memalloy

Licence: MIT license
Memory consistency modelling using Alloy

Programming Languages

ocaml
1615 projects
Alloy
16 projects
HTML
75241 projects
CSS
56736 projects
shell
77523 projects
python
139335 projects - #7 most used programming language
Makefile
30231 projects

Projects that are alternatives of or similar to memalloy

Unisimd Assembler
SIMD macro assembler unified for ARM, MIPS, PPC and x86
Stars: ✭ 63 (+173.91%)
Mutual labels:  x86, armv7, powerpc
Keypatch
Multi-architecture assembler for IDA Pro. Powered by Keystone Engine.
Stars: ✭ 939 (+3982.61%)
Mutual labels:  x86, powerpc
Arm now
arm_now is a qemu powered tool that allows instant setup of virtual machines on arm cpu, mips, powerpc, nios2, x86 and more, for reverse, exploit, fuzzing and programming purpose.
Stars: ✭ 719 (+3026.09%)
Mutual labels:  x86, powerpc
Reverse Engineering
This repository contains some of the executables that I've cracked.
Stars: ✭ 29 (+26.09%)
Mutual labels:  x86, armv7
Steed
[INACTIVE] Rust's standard library, free of C dependencies, for Linux systems
Stars: ✭ 520 (+2160.87%)
Mutual labels:  x86, powerpc
Capstone
Capstone disassembly/disassembler framework: Core (Arm, Arm64, BPF, EVM, M68K, M680X, MOS65xx, Mips, PPC, RISCV, Sparc, SystemZ, TMS320C64x, Web Assembly, X86, X86_64, XCore) + bindings.
Stars: ✭ 5,374 (+23265.22%)
Mutual labels:  x86, powerpc
Rappel
A linux-based assembly REPL for x86, amd64, armv7, and armv8
Stars: ✭ 818 (+3456.52%)
Mutual labels:  x86, armv7
Cross
“Zero setup” cross compilation and “cross testing” of Rust crates
Stars: ✭ 2,461 (+10600%)
Mutual labels:  x86, powerpc
reicast-emulator
Reicast was a multiplatform Sega Dreamcast emulator
Stars: ✭ 1,063 (+4521.74%)
Mutual labels:  x86, armv7
Keystone
Keystone assembler framework: Core (Arm, Arm64, Hexagon, Mips, PowerPC, Sparc, SystemZ & X86) + bindings
Stars: ✭ 1,654 (+7091.3%)
Mutual labels:  x86, powerpc
Unicorn
Unicorn CPU emulator framework (ARM, AArch64, M68K, Mips, Sparc, PowerPC, RiscV, X86)
Stars: ✭ 4,934 (+21352.17%)
Mutual labels:  x86, powerpc
Computelibrary
The Compute Library is a set of computer vision and machine learning functions optimised for both Arm CPUs and GPUs using SIMD technologies.
Stars: ✭ 2,123 (+9130.43%)
Mutual labels:  opencl, armv7
Easy Linux Pwn
A set of Linux binary exploitation tasks for beginners on various architectures
Stars: ✭ 353 (+1434.78%)
Mutual labels:  x86, powerpc
Ffmpeg Android
FFMpeg/FFprobe compiled for Android
Stars: ✭ 592 (+2473.91%)
Mutual labels:  x86, armv7
Maxine Vm
Maxine VM: A meta-circular research VM
Stars: ✭ 274 (+1091.3%)
Mutual labels:  x86, armv7
pinktrace
Pink's Tracing Library
Stars: ✭ 20 (-13.04%)
Mutual labels:  x86, powerpc
cross
“Zero setup” cross compilation and “cross testing” of Rust crates
Stars: ✭ 3,550 (+15334.78%)
Mutual labels:  x86, powerpc
alpine-php-fpm
Lightweight and optimised PHP-FPM (PHP 7.4, 8.0, 8.1) Docker images with essential extensions on top of latest Alpine Linux.
Stars: ✭ 53 (+130.43%)
Mutual labels:  x86, armv7
Bap
Binary Analysis Platform
Stars: ✭ 1,385 (+5921.74%)
Mutual labels:  x86, powerpc
Ataraxia
Simple and lightweight source-based multi-platform Linux distribution with musl libc.
Stars: ✭ 226 (+882.61%)
Mutual labels:  x86, powerpc
Licence Master branch Dev branch
License: MIT Build Status Build Status

System requirements

  • OCaml 4.07.0 or later (tested with 4.07.0)

  • OPAM packages xml-light, ocamlfind, and ocamlbuild (hint: opam install <package name>)

  • Python 2.7

  • Java runtime version 8 (tested with Java SE Development Kit 8u181).

  • Graphviz (hint: brew install graphviz)

  • Apache Ant, for building Alloy (hint: brew install ant)

Quick start

  1. Modify configure.sh to suit your OS.

  2. Run source configure.sh.

  3. Run make install. HTML documentation can now be browsed at doc/index.html.

  4. Run make quicktest. After a few minutes you should find some pictures of distinguishing executions in the png directory.

Converting .cat models to Alloy (.als) format

  • Each .cat file must begin with a description of the architecture being modelled. This must be one of: "BASIC", "C", "HW", "X86", "PPC", "ARM7", "ARM8", "PTX", "OpenCL", or "OCaml".

  • A reasonable fragment of the .cat language is supported.

    • You can define sets and relations via let x = e. Names of sets must begin with an uppercase letter, and names of relations must begin with a lowercase letter.

    • You can define functions via let f(r1,...,rn) = e. The name of the function must begin with an uppercase letter if the function returns a set, and must begin with a lowercase letter if the function returns a relation. Functions cannot return functions. Set-valued parameters must have a name beginning with an uppercase letter, and relation-valued parameters must begin with a lowercase letter. Parameters cannot be functions themselves.

    • You can define relations (but not sets) recursively via let x1 = e1 and ... and xn = en, and these are unrolled a fixed number of times when translating into Alloy (since Alloy only checks up to a finite bound anyway). The number of unrollings is set by the -u flag, which defaults to 3.

    • You can define a consistency axiom of the model called name via acyclic|irreflexive|empty e as name. You can define a 'definedness' axiom (i.e., one that must hold of every consistent execution or else the whole program is undefined) by prepending the statement above with undefined_unless, and you can define a 'deadness' axiom (i.e., one that must hold of an inconsistent execution in order to guarantee that the resultant litmus test has no other passing executions) by prepending the statement above with deadness_requires instead.

    • You can include the definitions and axioms of the submodel.cat file via include submodel.cat.

  • There are a few syntactic restrictions on .cat files.

    • The variable int, built into Herd, clashes with a keyword in Alloy, so is not allowed. You can use thd instead.

    • The variable X, built into Herd, clashes with another variable in Alloy, so is not allowed. You can use domain(atom) | range(atom) instead.

    • The variables L and A are used in Herd for 'release' and 'acquire' accesses in the Arm8 architecture, but these clash with the variables for 'local' accesses in OpenCL and 'atomic' accesses in C and OpenCL, respectively. Alloy does not allow variables to be re-used in this way, so you must use SCREL and SCACQ in the Arm8 architecture instead.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].