Global Index

D

G

H

J

K

Q

U

Y

Z

_

other

(131 entries)

Module Index

B

C

D

E

F

G

H

J

K

L

M

O

P

Q

R

T

U

V

W

Y

Z

_

other

(7 entries)

Variable Index

A

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(10 entries)

Library Index

B

C

D

E

F

G

H

I

J

K

L

M

N

P

Q

R

S

T

U

V

W

Y

Z

_

other

(3 entries)

Projection Index

C

D

F

G

H

J

K

N

P

Q

U

W

X

Y

Z

_

other

(19 entries)

Instance Index

A

B

D

E

F

G

H

I

J

K

L

M

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Section Index

A

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Abbreviation Index

A

B

C

D

E

G

H

J

K

L

N

O

Q

T

U

V

X

Y

Z

_

other

(16 entries)

Definition Index

D

G

H

J

K

Q

U

V

Y

Z

_

other

(62 entries)

Record Index

A

D

E

F

G

H

I

J

K

L

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Global Index

A

acquire_lock_conditional [definition, in ArchSemX86.OperationalX86TSO]
acquire_lock [definition, in ArchSemX86.OperationalX86TSO]
addr [projection, in ArchSemX86.OperationalX86TSO]
add_to_write_buffer [definition, in ArchSemX86.OperationalX86TSO]
add_to_mem_written [definition, in ArchSemX86.OperationalX86TSO]
all_buffers_empty [definition, in ArchSemX86.OperationalX86TSO]
Arch [module, in ArchSemX86.X86Inst]
ArchExtra [module, in ArchSemX86.X86Inst]
ArchExtra.pc_reg [definition, in ArchSemX86.X86Inst]
ArchExtra.reg_type_to_gen [definition, in ArchSemX86.X86Inst]
ArchExtra.reg_type_of_gen [definition, in ArchSemX86.X86Inst]
ArchExtra.reg_of_string [definition, in ArchSemX86.X86Inst]
archmodel [definition, in ArchSemX86.AxiomaticX86TSO]
atomic [projection, in ArchSemX86.AxiomaticX86TSO]
AxiomaticX86TSO [library]
axmodel [definition, in ArchSemX86.AxiomaticX86TSO]

B

Barriers [section, in ArchSemX86.AxiomaticX86TSO]
Barriers.et [variable, in ArchSemX86.AxiomaticX86TSO]
Barriers.nmth [variable, in ArchSemX86.AxiomaticX86TSO]
blocked [definition, in ArchSemX86.OperationalX86TSO]
buf [projection, in ArchSemX86.OperationalX86TSO]
buffer_empty [definition, in ArchSemX86.OperationalX86TSO]
buffer_entry [record, in ArchSemX86.OperationalX86TSO]

C

ca [definition, in ArchSemX86.AxiomaticX86TSO]
co [definition, in ArchSemX86.AxiomaticX86TSO]
coe [definition, in ArchSemX86.AxiomaticX86TSO]
coi [definition, in ArchSemX86.AxiomaticX86TSO]
consistent [record, in ArchSemX86.AxiomaticX86TSO]
consistent_ok_dec [instance, in ArchSemX86.AxiomaticX86TSO]
consistent_ok [definition, in ArchSemX86.AxiomaticX86TSO]
consistent_dec [instance, in ArchSemX86.AxiomaticX86TSO]

E

empty_write_buffer [definition, in ArchSemX86.OperationalX86TSO]
execution_step [definition, in ArchSemX86.OperationalX86TSO]
external_visibility [projection, in ArchSemX86.AxiomaticX86TSO]

F

flush_one_item_buffer [definition, in ArchSemX86.OperationalX86TSO]
fr [definition, in ArchSemX86.AxiomaticX86TSO]
fre [definition, in ArchSemX86.AxiomaticX86TSO]
fri [definition, in ArchSemX86.AxiomaticX86TSO]
from_archState [definition, in ArchSemX86.OperationalX86TSO]
full_instruction_order [abbreviation, in ArchSemX86.AxiomaticX86TSO]

I

IF [abbreviation, in ArchSemX86.AxiomaticX86TSO]
IMonFromSail [module, in ArchSemX86.X86Inst]
initial_reads [projection, in ArchSemX86.AxiomaticX86TSO]
int [abbreviation, in ArchSemX86.AxiomaticX86TSO]
internal_visibility [projection, in ArchSemX86.AxiomaticX86TSO]
IR [abbreviation, in ArchSemX86.AxiomaticX86TSO]
is_mfence [definition, in ArchSemX86.AxiomaticX86TSO]

L

lob [definition, in ArchSemX86.AxiomaticX86TSO]
lob1 [definition, in ArchSemX86.AxiomaticX86TSO]
lock [projection, in ArchSemX86.OperationalX86TSO]

M

M [abbreviation, in ArchSemX86.AxiomaticX86TSO]
mem [projection, in ArchSemX86.OperationalX86TSO]
memory_events_permitted [projection, in ArchSemX86.AxiomaticX86TSO]
memWritten [projection, in ArchSemX86.OperationalX86TSO]
mem_addr_modified [definition, in ArchSemX86.OperationalX86TSO]
MFENCE [abbreviation, in ArchSemX86.AxiomaticX86TSO]
mfence [definition, in ArchSemX86.AxiomaticX86TSO]
Model [section, in ArchSemX86.AxiomaticX86TSO]
Model [section, in ArchSemX86.OperationalX86TSO]
Model.cd [variable, in ArchSemX86.AxiomaticX86TSO]
Model.isem [variable, in ArchSemX86.OperationalX86TSO]
Model.ms [variable, in ArchSemX86.AxiomaticX86TSO]
Model.nmth [variable, in ArchSemX86.AxiomaticX86TSO]
Model.RunOutcome [section, in ArchSemX86.OperationalX86TSO]
Model.RunOutcome.eager [variable, in ArchSemX86.OperationalX86TSO]
Model.RunOutcome.tid [variable, in ArchSemX86.OperationalX86TSO]
Model.steps [section, in ArchSemX86.OperationalX86TSO]
Model.steps.term [variable, in ArchSemX86.OperationalX86TSO]
Model.threads [variable, in ArchSemX86.OperationalX86TSO]
mstate [record, in ArchSemX86.OperationalX86TSO]

N

NoCHERI [module, in ArchSemX86.X86Inst]
NoCHERI.no_cheri [definition, in ArchSemX86.X86Inst]
not_UB_dec [instance, in ArchSemX86.AxiomaticX86TSO]
not_UB [record, in ArchSemX86.AxiomaticX86TSO]
no_pending [definition, in ArchSemX86.OperationalX86TSO]

O

ob [definition, in ArchSemX86.AxiomaticX86TSO]
obs [definition, in ArchSemX86.AxiomaticX86TSO]
ob1 [definition, in ArchSemX86.AxiomaticX86TSO]
only_ms_if_allowed [projection, in ArchSemX86.AxiomaticX86TSO]
only_writes_in_coherence [projection, in ArchSemX86.AxiomaticX86TSO]
OperationalX86TSO [library]

P

pe [abbreviation, in ArchSemX86.AxiomaticX86TSO]
po [abbreviation, in ArchSemX86.AxiomaticX86TSO]
po_loc [definition, in ArchSemX86.AxiomaticX86TSO]

R

R [abbreviation, in ArchSemX86.AxiomaticX86TSO]
read_mem_with_store_forwarding [definition, in ArchSemX86.OperationalX86TSO]
read_mem_byte_with_store_forwarding [definition, in ArchSemX86.OperationalX86TSO]
read_byte_from_write_buffer [definition, in ArchSemX86.OperationalX86TSO]
read_byte_from_write_buffer_inner [definition, in ArchSemX86.OperationalX86TSO]
read_reg [definition, in ArchSemX86.OperationalX86TSO]
regs [projection, in ArchSemX86.OperationalX86TSO]
reg_internal' [projection, in ArchSemX86.AxiomaticX86TSO]
reg_internal_dec [instance, in ArchSemX86.AxiomaticX86TSO]
reg_internal [record, in ArchSemX86.AxiomaticX86TSO]
release_lock_conditional [definition, in ArchSemX86.OperationalX86TSO]
release_lock [definition, in ArchSemX86.OperationalX86TSO]
rf [definition, in ArchSemX86.AxiomaticX86TSO]
rfe [definition, in ArchSemX86.AxiomaticX86TSO]
rfi [definition, in ArchSemX86.AxiomaticX86TSO]
rfr [abbreviation, in ArchSemX86.AxiomaticX86TSO]
rfr_internal [projection, in ArchSemX86.AxiomaticX86TSO]
rmw [abbreviation, in ArchSemX86.AxiomaticX86TSO]
rrf [abbreviation, in ArchSemX86.AxiomaticX86TSO]
rrf_internal [projection, in ArchSemX86.AxiomaticX86TSO]
run_normal_then_eager [definition, in ArchSemX86.OperationalX86TSO]
run_eager_all [definition, in ArchSemX86.OperationalX86TSO]
run_eager_thread [definition, in ArchSemX86.OperationalX86TSO]
run_eager_thread_step [definition, in ArchSemX86.OperationalX86TSO]
run_outcome [definition, in ArchSemX86.OperationalX86TSO]
Rx [abbreviation, in ArchSemX86.AxiomaticX86TSO]

S

SA [module, in ArchSemX86.X86Inst]
sail_tiny_x86_sem [definition, in ArchSemX86.X86Inst]
SI [module, in ArchSemX86.X86Inst]
si [abbreviation, in ArchSemX86.AxiomaticX86TSO]
size [projection, in ArchSemX86.OperationalX86TSO]
step [definition, in ArchSemX86.OperationalX86TSO]

T

termThreads [projection, in ArchSemX86.OperationalX86TSO]
thread_has_lock [definition, in ArchSemX86.OperationalX86TSO]
to_terminated_archState [definition, in ArchSemX86.OperationalX86TSO]
to_archState [definition, in ArchSemX86.OperationalX86TSO]

V

val [projection, in ArchSemX86.OperationalX86TSO]

W

W [abbreviation, in ArchSemX86.AxiomaticX86TSO]
write_buffer_to_mem [definition, in ArchSemX86.OperationalX86TSO]
write_mem [definition, in ArchSemX86.OperationalX86TSO]
write_reg [definition, in ArchSemX86.OperationalX86TSO]
Wx [abbreviation, in ArchSemX86.AxiomaticX86TSO]

X

X86 [module, in ArchSemX86.X86Inst]
X86Inst [library]
x86_tso_modelc [definition, in ArchSemX86.OperationalX86TSO]
x86_tso_opmodel_eager [definition, in ArchSemX86.OperationalX86TSO]
x86_tso_opmodel [definition, in ArchSemX86.OperationalX86TSO]

Module Index

A

Arch [in ArchSemX86.X86Inst]
ArchExtra [in ArchSemX86.X86Inst]

I

IMonFromSail [in ArchSemX86.X86Inst]

N

NoCHERI [in ArchSemX86.X86Inst]

S

SA [in ArchSemX86.X86Inst]
SI [in ArchSemX86.X86Inst]

X

X86 [in ArchSemX86.X86Inst]

Variable Index

B

Barriers.et [in ArchSemX86.AxiomaticX86TSO]
Barriers.nmth [in ArchSemX86.AxiomaticX86TSO]

M

Model.cd [in ArchSemX86.AxiomaticX86TSO]
Model.isem [in ArchSemX86.OperationalX86TSO]
Model.ms [in ArchSemX86.AxiomaticX86TSO]
Model.nmth [in ArchSemX86.AxiomaticX86TSO]
Model.RunOutcome.eager [in ArchSemX86.OperationalX86TSO]
Model.RunOutcome.tid [in ArchSemX86.OperationalX86TSO]
Model.steps.term [in ArchSemX86.OperationalX86TSO]
Model.threads [in ArchSemX86.OperationalX86TSO]

Library Index

A

AxiomaticX86TSO

O

OperationalX86TSO

X

Projection Index

A

addr [in ArchSemX86.OperationalX86TSO]
atomic [in ArchSemX86.AxiomaticX86TSO]

B

buf [in ArchSemX86.OperationalX86TSO]

E

external_visibility [in ArchSemX86.AxiomaticX86TSO]

I

initial_reads [in ArchSemX86.AxiomaticX86TSO]
internal_visibility [in ArchSemX86.AxiomaticX86TSO]

L

lock [in ArchSemX86.OperationalX86TSO]

M

mem [in ArchSemX86.OperationalX86TSO]
memory_events_permitted [in ArchSemX86.AxiomaticX86TSO]
memWritten [in ArchSemX86.OperationalX86TSO]

O

only_ms_if_allowed [in ArchSemX86.AxiomaticX86TSO]
only_writes_in_coherence [in ArchSemX86.AxiomaticX86TSO]

R

regs [in ArchSemX86.OperationalX86TSO]
reg_internal' [in ArchSemX86.AxiomaticX86TSO]
rfr_internal [in ArchSemX86.AxiomaticX86TSO]
rrf_internal [in ArchSemX86.AxiomaticX86TSO]

S

size [in ArchSemX86.OperationalX86TSO]

T

termThreads [in ArchSemX86.OperationalX86TSO]

V

val [in ArchSemX86.OperationalX86TSO]

Instance Index

C

consistent_ok_dec [in ArchSemX86.AxiomaticX86TSO]
consistent_dec [in ArchSemX86.AxiomaticX86TSO]

N

not_UB_dec [in ArchSemX86.AxiomaticX86TSO]

R

reg_internal_dec [in ArchSemX86.AxiomaticX86TSO]

Section Index

B

Barriers [in ArchSemX86.AxiomaticX86TSO]

M

Model [in ArchSemX86.AxiomaticX86TSO]
Model [in ArchSemX86.OperationalX86TSO]
Model.RunOutcome [in ArchSemX86.OperationalX86TSO]
Model.steps [in ArchSemX86.OperationalX86TSO]

Abbreviation Index

F

full_instruction_order [in ArchSemX86.AxiomaticX86TSO]

I

IF [in ArchSemX86.AxiomaticX86TSO]
int [in ArchSemX86.AxiomaticX86TSO]
IR [in ArchSemX86.AxiomaticX86TSO]

M

M [in ArchSemX86.AxiomaticX86TSO]
MFENCE [in ArchSemX86.AxiomaticX86TSO]

P

pe [in ArchSemX86.AxiomaticX86TSO]
po [in ArchSemX86.AxiomaticX86TSO]

R

R [in ArchSemX86.AxiomaticX86TSO]
rfr [in ArchSemX86.AxiomaticX86TSO]
rmw [in ArchSemX86.AxiomaticX86TSO]
rrf [in ArchSemX86.AxiomaticX86TSO]
Rx [in ArchSemX86.AxiomaticX86TSO]

S

si [in ArchSemX86.AxiomaticX86TSO]

W

W [in ArchSemX86.AxiomaticX86TSO]
Wx [in ArchSemX86.AxiomaticX86TSO]

Definition Index

A

acquire_lock_conditional [in ArchSemX86.OperationalX86TSO]
acquire_lock [in ArchSemX86.OperationalX86TSO]
add_to_write_buffer [in ArchSemX86.OperationalX86TSO]
add_to_mem_written [in ArchSemX86.OperationalX86TSO]
all_buffers_empty [in ArchSemX86.OperationalX86TSO]
ArchExtra.pc_reg [in ArchSemX86.X86Inst]
ArchExtra.reg_type_to_gen [in ArchSemX86.X86Inst]
ArchExtra.reg_type_of_gen [in ArchSemX86.X86Inst]
ArchExtra.reg_of_string [in ArchSemX86.X86Inst]
archmodel [in ArchSemX86.AxiomaticX86TSO]
axmodel [in ArchSemX86.AxiomaticX86TSO]

B

blocked [in ArchSemX86.OperationalX86TSO]
buffer_empty [in ArchSemX86.OperationalX86TSO]

C

ca [in ArchSemX86.AxiomaticX86TSO]
co [in ArchSemX86.AxiomaticX86TSO]
coe [in ArchSemX86.AxiomaticX86TSO]
coi [in ArchSemX86.AxiomaticX86TSO]
consistent_ok [in ArchSemX86.AxiomaticX86TSO]

E

empty_write_buffer [in ArchSemX86.OperationalX86TSO]
execution_step [in ArchSemX86.OperationalX86TSO]

F

flush_one_item_buffer [in ArchSemX86.OperationalX86TSO]
fr [in ArchSemX86.AxiomaticX86TSO]
fre [in ArchSemX86.AxiomaticX86TSO]
fri [in ArchSemX86.AxiomaticX86TSO]
from_archState [in ArchSemX86.OperationalX86TSO]

I

is_mfence [in ArchSemX86.AxiomaticX86TSO]

L

lob [in ArchSemX86.AxiomaticX86TSO]
lob1 [in ArchSemX86.AxiomaticX86TSO]

M

mem_addr_modified [in ArchSemX86.OperationalX86TSO]
mfence [in ArchSemX86.AxiomaticX86TSO]

N

NoCHERI.no_cheri [in ArchSemX86.X86Inst]
no_pending [in ArchSemX86.OperationalX86TSO]

O

ob [in ArchSemX86.AxiomaticX86TSO]
obs [in ArchSemX86.AxiomaticX86TSO]
ob1 [in ArchSemX86.AxiomaticX86TSO]

P

po_loc [in ArchSemX86.AxiomaticX86TSO]

R

read_mem_with_store_forwarding [in ArchSemX86.OperationalX86TSO]
read_mem_byte_with_store_forwarding [in ArchSemX86.OperationalX86TSO]
read_byte_from_write_buffer [in ArchSemX86.OperationalX86TSO]
read_byte_from_write_buffer_inner [in ArchSemX86.OperationalX86TSO]
read_reg [in ArchSemX86.OperationalX86TSO]
release_lock_conditional [in ArchSemX86.OperationalX86TSO]
release_lock [in ArchSemX86.OperationalX86TSO]
rf [in ArchSemX86.AxiomaticX86TSO]
rfe [in ArchSemX86.AxiomaticX86TSO]
rfi [in ArchSemX86.AxiomaticX86TSO]
run_normal_then_eager [in ArchSemX86.OperationalX86TSO]
run_eager_all [in ArchSemX86.OperationalX86TSO]
run_eager_thread [in ArchSemX86.OperationalX86TSO]
run_eager_thread_step [in ArchSemX86.OperationalX86TSO]
run_outcome [in ArchSemX86.OperationalX86TSO]

S

sail_tiny_x86_sem [in ArchSemX86.X86Inst]
step [in ArchSemX86.OperationalX86TSO]

T

thread_has_lock [in ArchSemX86.OperationalX86TSO]
to_terminated_archState [in ArchSemX86.OperationalX86TSO]
to_archState [in ArchSemX86.OperationalX86TSO]

W

write_buffer_to_mem [in ArchSemX86.OperationalX86TSO]
write_mem [in ArchSemX86.OperationalX86TSO]
write_reg [in ArchSemX86.OperationalX86TSO]

X

x86_tso_modelc [in ArchSemX86.OperationalX86TSO]
x86_tso_opmodel_eager [in ArchSemX86.OperationalX86TSO]
x86_tso_opmodel [in ArchSemX86.OperationalX86TSO]

Record Index

B

buffer_entry [in ArchSemX86.OperationalX86TSO]

C

consistent [in ArchSemX86.AxiomaticX86TSO]

M

mstate [in ArchSemX86.OperationalX86TSO]

N

not_UB [in ArchSemX86.AxiomaticX86TSO]

R

reg_internal [in ArchSemX86.AxiomaticX86TSO]

Global Index

D

G

H

J

K

Q

U

Y

Z

_

other

(131 entries)

Module Index

B

C

D

E

F

G

H

J

K

L

M

O

P

Q

R

T

U

V

W

Y

Z

_

other

(7 entries)

Variable Index

A

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(10 entries)

Library Index

B

C

D

E

F

G

H

I

J

K

L

M

N

P

Q

R

S

T

U

V

W

Y

Z

_

other

(3 entries)

Projection Index

C

D

F

G

H

J

K

N

P

Q

U

W

X

Y

Z

_

other

(19 entries)

Instance Index

A

B

D

E

F

G

H

I

J

K

L

M

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(4 entries)

Section Index

A

C

D

E

F

G

H

I

J

K

L

N

O

P

Q

R

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

Abbreviation Index

A

B

C

D

E

G

H

J

K

L

N

O

Q

T

U

V

X

Y

Z

_

other

(16 entries)

Definition Index

D

G

H

J

K

Q

U

V

Y

Z

_

other

(62 entries)

Record Index

A

D

E

F

G

H

I

J

K

L

O

P

Q

S

T

U

V

W

X

Y

Z

_

other

(5 entries)

This page has been generated by coqdoc